proposition: Lemma le_trans_ereal : ssrbool.transitive le_ereal.
proof: Proof. case=> [?||][?||][?||] //=; rewrite -?comparabler0; first exact: le_trans. by move=> /le_comparable cmp /(comparabler_trans cmp). by move=> cmp /ge_comparable /comparabler_trans; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed