proposition: Theorem in_mkRect: forall n m p, In p (mkRect n m) -> exists p1, exists p2, 0 <= p1 <= Z_of_nat n /\ 0 <= p2 <= Z_of_nat m /\ p = (p1, p2).
proof: Proof. intros n m1 p; elim n; clear n; simpl. rewrite <- app_nil_end; intros H1. case in_mkLine with (1 := H1). intros p2 (H2, H3); exists 0; exists p2; auto with zarith. intros n Rec H1. case in_app_or with (1 := H1); intros H2. case in_mkLine with (1 := H2). intros p2 (H3, H4); exists (Z_of_nat (S n)); exists p2; subst; simpl; auto with zarith. case Rec with (1 := H2); auto. intros p1 (p2, (H3, (H4, H5))); exists p1; exists p2; repeat split. 1, 3-5: auto with zarith. change (p1 <= Z_of_nat (S n)). rewrite inj_S; auto with zarith. Qed.
imports: ZArith Znumtheory Tactic Wf_nat ListAux UList FGroup EGroup IGroup