proposition: Theorem mL_length : length mL = Z.abs_nat (m * m).
proof: Proof. unfold mL; rewrite mkRect_length; simpl; apply inj_eq_rev. repeat (rewrite inj_mult || rewrite inj_plus || rewrite inj_Zabs_nat || rewrite Z.abs_eq); simpl. 2-3: auto with zarith. eq_tac; auto with zarith. Qed.
imports: ZArith Znumtheory Tactic Wf_nat ListAux UList FGroup EGroup IGroup