proposition: Theorem in_mL: forall p, In p mL-> exists p1, exists p2, 0 <= p1 < m /\ 0 <= p2 < m /\ p = (p1, p2).
proof: Proof. unfold mL; intros p H1; case in_mkRect with (1 := H1). repeat (rewrite inj_Zabs_nat || rewrite Z.abs_eq); auto with zarith. intros p1 (p2, ((H2, H3), ((H4, H5), H6))); exists p1; exists p2; repeat split; auto with zarith. Qed.
imports: ZArith Znumtheory Tactic Wf_nat ListAux UList FGroup EGroup IGroup