proposition: Theorem rect_aux2: forall x1 x2 y1 y2, y1 < size -> y2 < size -> mod x1 h * w + mod y1 w = mod x2 h * w + mod y2 w -> div x1 h * h + div y1 w = div x2 h * h + div y2 w -> x1 = x2 /\ y1 = y2.
proof: Proof. Proof with auto with arith. intros x1 x2 y1 y2 V1 V2 H1 H2. assert (U1: 0 < h). generalize V1; unfold size; case h; simpl... intros tmp; contradict tmp... assert (U2: 0 < w). generalize V1; unfold size; case w; simpl... rewrite Nat.mul_0_r; intros tmp; contradict tmp... assert (Eq1: mod x1 h = mod x2 h). apply lexico_mult with (3 := H1); apply mod_lt... assert (Eq2: div x1 h = div x2 h). apply lexico_mult with (3 := H2); apply div_lt; rewrite Nat.mul_comm... split; [ rewrite (div_mod_correct x1 h); try rewrite (div_mod_correct x2 h) | rewrite (div_mod_correct y1 w); try rewrite (div_mod_correct y2 w)]... replace (div y1 w) with (div y2 w)... f_equal... apply Nat.add_cancel_l with (mod x1 h * w). pattern (mod x1 h) at 2; rewrite Eq1... apply Nat.add_cancel_l with (div x1 h * h). pattern (div x1 h) at 1; rewrite Eq2... Qed.
imports: List UList Permutation Div OrderedList ListOp Lia