proposition: Lemma cycle2g x : #[x] = 2 -> <[x]> = [set 1; x].
proof: Proof. by move=> ox; apply/setP=> y; rewrite cycle_traject ox !inE mulg1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)