proposition: Theorem gen_rect_correct: forall l i z, i < size -> (In l (gen_rect i z) <-> exists i1, exists j1, l = L (Pos (h * div i h + i1) (w * mod i h + j1)) z /\ i1 < h /\ j1 < w).
proof: Proof. intros ((x, y), z1) i z H; unfold gen_rect; split; intros H1. generalize (fold_insert2 _ (fun p => (L (shift p (h * div i h) (w * mod i h)) z)) _ _ H1). clear H1; intros (b, (Hb, Hb1)). match type of Hb with In ?X cross => case (cross_correct X); intros tmp _; case (tmp Hb); clear tmp end. intros i1 (j1, (H4, (H5, H6))); exists i1; exists j1; intros; subst; auto with arith. case H1; intros i1 (j1, (H2, (H3, H4))); clear H1. rewrite H2. match goal with |- In (L (Pos (?X + ?Y) (?Z + ?T)) ?U) ?V => change (In (L (shift (Pos Y T) X Z) U) V) end. apply fold_insert1 with (f := (fun p => (L (shift p (h * div i h) (w * mod i h)) z))); auto. case (cross_correct (Pos i1 j1)); intros _ tmp; apply tmp; clear tmp. exists i1; exists j1; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia