proposition: Theorem rect_aux1: forall x y, x < size -> y < size -> div x h * h + div y w < size.
proof: Proof. intros x y H H1; unfold size; rewrite (Nat.mul_comm h); apply mult_lt_plus. apply div_lt; auto. apply div_lt; auto. rewrite Nat.mul_comm; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia