let n be non zero Nat; :: thesis: card (Dihedral_group n) = 2 * n
thus card (Dihedral_group n) = (card (INT.Group n)) * (card (INT.Group 2)) by Th74
.= 2 * n ; :: thesis: verum