proposition: Lemma lt_def_ereal x y : lt_ereal x y = (y != x) && le_ereal x y.
proof: Proof. by case: x y => [?||][?||] //=; rewrite lt_def eqe. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed