proposition: Lemma num_lte_minr a x y : a < mine x%:num y%:num = (a < x%:num) && (a < y%:num).
proof: Proof. by rewrite -comparable_lt_minr// ereal_comparable. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed