proposition: Theorem lagrange: (g_order G | (g_order H)).
proof: Proof. unfold g_order. rewrite Permutation.permutation_length with (l := H.(s)) (m:= mkGH). case mkGH_length; intros x H1; exists (Z_of_nat x). rewrite H1; rewrite Zmult_comm; apply inj_mult. apply ulist_incl2_permutation; auto. apply ulist_mkGH. apply mkGH_incl. apply incl_mkGH. Qed.
imports: List UList ListAux ZArith Znumtheory NatAux FGroup