proposition: Theorem groupExp_closed : forall k, In (g^k) (getSupport RndGrpElem).
proof: Proof. intuition. erewrite groupExp_mod. simpl. eapply in_getUnique. eapply in_flatten. econstructor. split. eapply in_map_iff. econstructor. split. eauto. eapply filter_In. split. eapply in_getUnique. eapply in_flatten. econstructor. split. eapply in_map_iff. econstructor. split. eapply eq_refl. eapply in_getAllBvectors. simpl. left. eapply eq_refl. 2:{ rewrite bvToNat_natToBv_inverse. simpl. left. eapply eq_refl. eapply lognat_monotonic. eapply modNat_lt. } rewrite bvToNat_natToBv_inverse. unfold ltNatBool. destruct (lt_dec (modNat k order) order); trivial. exfalso. eapply n. eapply modNat_lt. eapply lognat_monotonic. eapply modNat_lt. apply g_generator. Qed.
imports: FCF.FCF FCF.GroupTheory