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