proposition: Lemma num_lt_minr a x y : a < Num.min x%:num y%:num = (a < x%:num) && (a < y%:num).
proof: Proof. by rewrite -comparable_lt_minr// real_comparable. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)