proposition: Lemma lecr_mulf2r (z : F) (x y : creal F) : (x <= y)%CR -> 0 <= z -> (x * z%:CR <= y * z%:CR)%CR.
proof: Proof. move=> lexy. rewrite le_eqVlt; case/orP=> [/eqP <- | lt0z]; first by rewrite !mul_creal0. move => h; apply: lexy. have aux t : (t == t * z%:CR * z^-1%:CR)%CR. rewrite -mulcrA -cst_crealM mulfV ?mul_creal1 //; move: lt0z; rewrite lt0r. by case/andP. rewrite [x]aux {}[y]aux; apply: ltcr_mul2r => //; apply/lt_creal_cst. by rewrite invr_gt0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)