proposition: Lemma num_lee_maxr a x y : a <= maxe x%:num y%:num = (a <= x%:num) || (a <= y%:num).
proof: Proof. by rewrite -comparable_le_maxr// ereal_comparable. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed