proposition: Lemma addr_gtcr0 (x y : creal F) : (0 < x -> 0 < y -> 0 < x + y)%CR.
proof: Proof. move=> lt_0x lt_0y. have := ltcr_add2r y lt_0x; rewrite add_0creal => h. by apply: lt_creal_trans h. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)