proposition: Lemma ltcr_spaddl (y x z : creal F) : (0 < x -> y <= z -> y < x + z)%CR.
proof: Proof. move=> *; rewrite -[y]add_0creal; exact: ltcr_le_add. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)