proposition: Theorem next_ch_points_hd : ∀ pt₁ pt₂ pt₃ pts₁ seg, lower_convex_hull_points [pt₁ … pts₁] = Some (mkns pt₂ pt₃ seg) → pt₁ = pt₂.
proof: Proof. intros * Hnp; simpl in Hnp. destruct pts₁ as [| pt₄ pts]; [ easy | ]. injection Hnp; clear Hnp; intros H1 H2 H3. specialize (minimised_slope_beg_pt pt₁ pt₄ pts) as Hm. now rewrite <- H3, Hm. Qed.
imports: Utf8 QArith Sorting Misc ConvexHull Slope_base