proposition: Lemma coversP x y : reflect (x < y /\ (forall z, ~(x < z < y))) (covers x y).
proof: Proof. apply (iffP andP) => /= [[ltxy /forallP Hcovers] | [ltxy Hcovers]]. - by split => // z; apply/negP. - by split => //; apply/forallP => z; apply/negP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools