proposition: Lemma lecr_mulf2l (z : F) (x y : creal F) : (x <= y)%CR -> 0 <= z -> (z%:CR * x <= z%:CR * y)%CR.
proof: Proof. by rewrite ![(z%:CR * _)%CR]mulcrC; apply: lecr_mulf2r. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)