proposition: Lemma leR_pmul2r m n1 n2 : 0 < m -> (n1 * m <= n2 * m) <-> (n1 <= n2).
proof: Proof. by move=> m0; split; [exact: Rmult_le_reg_r | exact/Rmult_le_compat_r/ltRW]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)