proposition: Lemma coversEV x y : covers x y -> forall z, x <= z <= y -> z = x \/ z = y.
proof: Proof. move=> /coversP[ltxy Hcovers] z /andP[]. rewrite le_eqVlt => /orP[/eqP -> | ltxz]; first by left. rewrite le_eqVlt => /orP[/eqP -> | ltzy]; first by right. by exfalso; apply: (Hcovers z); rewrite ltxz ltzy. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools