proposition: Lemma lecr_lt_trans (y x z : creal F): (x <= y)%CR -> (y < z)%CR -> (x < z)%CR.
proof: Proof. move=> lexy ltyz; pose_big_enough i. have hpos : 0 < diff ltyz / 2%:~R. apply: divr_gt0; rewrite ?ltr0Sn //; exact: diff_gt0. apply: (@lt_crealP _ ((diff ltyz) / 2%:~R) i i) => //=. apply: le_trans (@diffP _ _ _ ltyz _ _ _) => //; rewrite -lerBrDr. suff <- : y i + diff ltyz / 2%:~R = y i + diff ltyz - diff ltyz / 2%:~R. by apply: ltW; apply: le_modP. apply/eqP; rewrite eq_sym subr_eq -addrA -mulrDr. have <- : 1 = 2%:~R^-1 + 2%:~R^-1 :> F by rewrite [LHS](splitf 2) div1r. by rewrite mulr1. by close. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)