proposition: Lemma eq_creal_ext (x y : creal F) : x =1 y -> (x == y)%CR.
proof: Proof. move=> heq; apply/eq_crealP; exists (fun _ => 0%N) => * /=. by rewrite heq subrr normr0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)