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