proposition: Lemma mulr_gtcr0 (x y : creal F) : (0 < x -> 0 < y -> 0 < x * y)%CR.
proof: Proof. move=> lt_0x lt_0y; pose_big_enough i. apply: (@lt_crealP _ ((diff lt_0x) * (diff lt_0y)) i i) => //=. - apply: mulr_gt0; exact: diff_gt0. rewrite add0r; apply: ler_pM. - by apply: ltW; apply: diff_gt0. - by apply: ltW; apply: diff_gt0. - by rewrite -[X in X <= _]add0r -[0]/((0%:CR)%CR i) 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)