proposition: Lemma cyclic_small G : #|G| <= 3 -> cyclic G.
proof: Proof. rewrite 4!(ltnS, leq_eqVlt) -trivg_card_le1 orbA orbC. case/predU1P=> [-> | oG]; first exact: cyclic1. by apply: prime_cyclic; case/pred2P: oG => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm automorphism quotient gproduct ssralg) mathcomp(finalg zmodp poly)