proposition: Lemma lecr_lt_add (x y z t : creal F) : (x <= y -> z < t -> x + z < y + t)%CR.
proof: Proof. move=> lxy lzt; apply: (@lecr_lt_trans (y + z)%CR); last exact: ltcr_add2l. move/(ltcr_add2l (-z)%CR)=> abs; apply: lxy; move: abs. by rewrite ![(- z + _)%CR]addcrC -!addcrA addcrN !add_creal0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)