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