proposition: Lemma ltcr_mul2r (z x y : creal F) : (x < y)%CR -> (0 < z)%CR -> (x * z < y * z)%CR.
proof: Proof. move=> ltxy lt0z; pose_big_enough i. apply: (@lt_crealP _ ((diff ltxy) * (diff lt0z)) i i) => //=. - apply: mulr_gt0; exact: diff_gt0. rewrite -lerBDl -mulrBl; apply: ler_pM. - by apply: ltW; apply: diff_gt0. - by apply: ltW; apply: diff_gt0. - by rewrite lerBDl diffP. - by rewrite -[X in X <= _]add0r -[0]/((0%:CR)%CR i) diffP. by close. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)