proposition: Lemma ltcr_le_add (x y z t : creal F) : (x < y -> z <= t -> x + z < y + t)%CR.
proof: Proof. move=> *; rewrite [X in (X < _)%CR]addcrC [X in (_ < X)%CR]addcrC. by apply: lecr_lt_add. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)