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