proposition: Lemma add_crealP (x y : creal) : creal_axiom (fun i => x i + y i).
proof: Proof. exists_big_modulus m F. move=> e i j he hi hj; rewrite opprD addrAC addrA -addrA [- _ + _]addrC. by rewrite split_norm_add ?cauchymodP ?divrn_gt0. by close. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)