proposition: Lemma eq_creal_inv (x y : creal) (x_neq0 : x != 0) (y_neq0 : y != 0) : (x == y) -> (x_neq0^-1 == y_neq0^-1).
proof: Proof. move=> eq_xy; apply: eq_crealP; exists_big_modulus m F. move=> e i e_gt0 hi /=. rewrite -(@ltr_pmul2r _ (lbound x_neq0 * lbound y_neq0)); do ?by rewrite ?pmulr_rgt0 ?lbound_gt0. apply: le_lt_trans (_ : `|(x i)^-1 - (y i)^-1| * (`|x i| * `|y i|) < _). rewrite ler_wpmul2l ?normr_ge0 //. apply: le_trans (_ : `|x i| * lbound y_neq0 <= _). by rewrite ler_wpmul2r ?lbound_ge0 ?lbound0P. by rewrite ler_wpmul2l ?normr_ge0 ?lbound0P. rewrite -!normrM mulrBl mulKf ?creal_neq0_always //. rewrite mulrCA mulVf ?mulr1 ?creal_neq0_always //. by rewrite distrC eq_modP ?pmulr_rgt0 ?lbound_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)