proposition: Theorem mkGH_length: divide (length G.(s)) (length mkGH).
proof: Proof. unfold mkGH; elim H.(s); simpl. exists 0%nat; auto with arith. intros a l1 (c, H1); case (In_dec A_dec a (mkList G.(s) l1)); intros H2. exists c; auto. exists (1 + c)%nat; rewrite ListAux.length_app; rewrite ListAux.length_map; rewrite H1; ring. Qed.
imports: List UList ListAux ZArith Znumtheory NatAux FGroup