proposition: Theorem mL_in: forall p q, 0 <= p < m -> 0 <= q < m -> (In (p, q) mL).
proof: Proof. intros p q (H1, H2) (H3, H4); unfold mL; apply mkRect_in; rewrite inj_Zabs_nat; rewrite Z.abs_eq; auto with zarith. Qed.
imports: ZArith Znumtheory Tactic Wf_nat ListAux UList FGroup EGroup IGroup