proposition: Lemma ltcr_le_trans (y x z : creal F): (x < y -> y <= z -> x < z)%CR.
proof: Proof. move=> ltxy leyz; pose_big_enough i. have hpos : 0 < diff ltxy / 2%:~R. apply: divr_gt0; rewrite ?ltr0Sn //; exact: diff_gt0. apply: (@lt_crealP _ ((diff ltxy) / 2%:~R) i i) => //=. have -> : x i + diff ltxy / 2%:~R = x i + diff ltxy - diff ltxy / 2%:~R. 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. rewrite lerBlDr; apply: le_trans (diffP _ _) _ => //; apply: ltW. by apply: le_modP. by close. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)