proposition: Lemma inv_crealP (x : creal) (x_neq0 : x != 0) : creal_axiom (fun i => (x i)^-1).
proof: Proof. pose d := lbound x_neq0. exists_big_modulus m F. move=> e i j e_gt0 hi hj. have /andP[xi_neq0 xj_neq0] : (x i != 0) && (x j != 0). by rewrite -!normr_gt0 !(lt_le_trans _ (lbound0_of x_neq0)) ?lbound_gt0. rewrite -(@ltr_pmul2r _ `|x i * x j|); last by rewrite normr_gt0 mulf_neq0. rewrite -normrM !mulrBl mulrA mulVf // mulrCA mulVf // mul1r mulr1. apply: lt_le_trans (_ : e * d ^+ 2 <= _). by apply: cauchymodP; rewrite // !pmulr_rgt0 ?lbound_gt0. rewrite ler_wpmul2l ?(ltW e_gt0) // normrM. have /(_ j) hx /= := lbound0_of x_neq0. have -> // := (le_trans (ler_wpmul2l _ (hx _ _))). by rewrite ltW // lbound_gt0. by rewrite ler_wpmul2r ?normr_ge0 // lbound0P. 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)