`{!TrivialApart A} x y : x < y <-> x ≤ y /\ x <> y. Proof. transitivity (x <= y /\ apart x y). - apply lt_iff_le_apart. - split;intros [E1 E2];split;trivial;apply trivial_apart;trivial. Qed.
Require Import