proposition: Lemma le_anti_ereal : ssrbool.antisymmetric le_ereal.
proof: Proof. by case=> [?||][?||]/=; rewrite ?andbF => // /le_anti ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed