proposition: Theorem HdRel_app : ∀ A (R : A → A → Prop) a l₁ l₂, HdRel R a l₁ → HdRel R a l₂ → HdRel R a (l₁ ++ l₂).
proof: Proof. intros A R a l₁ l₂ H₁ H₂. destruct l₁ as [| b]; [ assumption | constructor ]. apply HdRel_inv in H₁; assumption. Qed.
imports: Utf8 QArith Sorting Misc ConvexHull Slope_base