proposition: Lemma leR_pmull m n : 1 <= n -> 0 <= m -> m <= n * m.
proof: Proof. move=> n1 m0; case/boolP : (m == 0) => [/eqP ->|m0']; first by rewrite mulR0; exact/Rle_refl. by rewrite -{1}(mul1R m) leR_pmul2r // ltR_neqAle; split => //; apply/eqP; rewrite eq_sym. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)