proposition: Lemma ltcr_add2l (z x y : creal F) : (x < y)%CR -> (z + x < z + y)%CR.
proof: Proof. move=> lt_xy; pose_big_enough i. apply: (@lt_crealP _ (diff lt_xy) i i); rewrite ?diff_gt0 //=. rewrite -addrA lerD2l diffP //. by close. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)