proposition: Theorem mkRect_ulist: forall n m, ulist (mkRect n m).
proof: Proof. intros n; elim n; simpl; auto. intros n1; rewrite <- app_nil_end; apply mkLine_ulist; auto. intros n1 Rec m1; apply ulist_app; auto. apply mkLine_ulist. intros a H1 H2. case in_mkLine with (1 := H1); intros p1 ((H3, H4), H5). case in_mkRect with (1 := H2); intros p2 (p3, ((H6, H7), ((H8, H9), H10))). subst; injection H10; clear H10; intros; subst. contradict H7. change (~ Z_of_nat (S n1) <= Z_of_nat n1). rewrite inj_S; auto with zarith. Qed.
imports: ZArith Znumtheory Tactic Wf_nat ListAux UList FGroup EGroup IGroup