proposition: Lemma subcr_eq0 (x y : creal F) : (x - y == 0)%CR <-> (x == y)%CR.
proof: Proof. split => h. rewrite -[y]add_creal0 -h; apply: eq_creal_ext=> i /=; rewrite addrCA subrr. by rewrite addr0. by rewrite h; apply: eq_creal_ext=> i /=; rewrite subrr. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)