proposition: Theorem mkRect_in: forall n m p q, 0 <= p <= Z_of_nat n -> 0 <= q <= Z_of_nat m -> (In (p, q) (mkRect n m)).
proof: Proof. intros n m1; elim n; simpl. intros p q (H1, H2) (H3, H4); replace p with 0; auto with zarith. rewrite <- app_nil_end; apply mkLine_in; auto. intros n1 Rec p q (H1, H2) (H3, H4). case (Zle_lt_or_eq p (Z_of_nat (S n1))); auto with zarith; intros H5. rewrite inj_S in H5; apply in_or_app; auto with zarith. apply in_or_app; left; subst; apply mkLine_in; auto with zarith. Qed.
imports: ZArith Znumtheory Tactic Wf_nat ListAux UList FGroup EGroup IGroup