proposition: Theorem slope_cmp_flatten : ∀ x₁ y₁ x₂ y₂ x₃ y₃ x₄ y₄, x₁ < x₂ → x₃ < x₄ → (slope_expr (x₁, y₁) (x₂, y₂) ?= slope_expr (x₃, y₃) (x₄, y₄)) = (y₂ * x₄ + y₁ * x₃ + y₃ * x₂ + y₄ * x₁ ?= y₄ * x₂ + y₃ * x₁ + y₁ * x₄ + y₂ * x₃).
proof: Proof. intros x₁ y₁ x₂ y₂ x₃ y₃ x₄ y₄ Hlt₁₂ Hlt₃₄. unfold slope_expr; simpl. rewrite Qcmp_shift_mult_r; [ idtac | apply Qlt_minus; assumption ]. rewrite Qmult_div_swap. rewrite Qcmp_shift_mult_l; [ idtac | apply Qlt_minus; assumption ]. repeat rewrite Qmult_minus_distr_l. repeat rewrite Qmult_minus_distr_r. repeat rewrite Qminus_minus_assoc. repeat rewrite <- Qplus_minus_swap. repeat rewrite <- Qcmp_plus_minus_cmp_r. repeat rewrite <- Qplus_minus_swap. repeat rewrite <- Qplus_cmp_cmp_minus_r. reflexivity. Qed.
imports: Utf8 QArith Slope_base Misc