proposition: Theorem slope_cmp_norm₁₃₂₃ : ∀ x₁ y₁ x₂ y₂ x₃ y₃, x₁ < x₂ < x₃ → (slope_expr (x₁, y₁) (x₃, y₃) ?= slope_expr (x₂, y₂) (x₃, y₃)) = (x₁ * y₃ + x₂ * y₁ + x₃ * y₂ ?= x₁ * y₂ + x₂ * y₃ + x₃ * y₁).
proof: Proof. intros x₁ y₁ x₂ y₂ x₃ y₃ (Hlt₁, Hlt₂). assert (x₁ < x₃) as Hlt₃ by (eapply Qlt_trans; eassumption). rewrite slope_cmp_flatten; [ idtac | assumption | assumption ]. repeat rewrite <- Qplus_assoc. rewrite <- Qplus_cmp_compat_l. repeat rewrite Qplus_assoc. setoid_replace (y₁ * x₂ + y₂ * x₃ + y₃ * x₁) with (x₁ * y₃ + x₂ * y₁ + x₃ * y₂) by ring. setoid_replace (y₂ * x₁ + y₁ * x₃ + y₃ * x₂) with (x₁ * y₂ + x₂ * y₃ + x₃ * y₁) by ring. reflexivity. Qed.
imports: Utf8 QArith Slope_base Misc