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 ]. rewrite <- Qplus_assoc, Qplus_comm, Qplus_assoc. remember (y₁ * x₂ + y₃ * x₁ + y₂ * x₃ + y₁ * x₁) as t. rewrite <- Qplus_assoc, Qplus_comm, Qplus_assoc; subst t. rewrite <- Qplus_cmp_compat_r. 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