proposition: Lemma algebraic_inv u : algebraicOver FtoE u -> algebraicOver FtoE u^-1.
proof: Proof. have [-> | /expf_neq0 nz_u_n] := eqVneq u 0; first by rewrite invr0. case=> p nz_p pu0; exists (Poly (rev p)). apply/eqP=> /polyP/(_ 0); rewrite coef_Poly coef0 nth_rev ?size_poly_gt0 //. by apply/eqP; rewrite subn1 lead_coef_eq0. apply/eqP/(mulfI (nz_u_n (size p).-1)); rewrite mulr0 -(rootP pu0). rewrite (@horner_coef_wide _ (size p)); last first. by rewrite size_map_poly -(size_rev p) size_Poly. rewrite horner_coef mulr_sumr size_map_poly. rewrite [rhs in _ = rhs](reindex_inj rev_ord_inj) /=. apply: eq_bigr => i _; rewrite !coef_map coef_Poly nth_rev // mulrCA. by congr (_ * _); rewrite -{1}(subnKC (valP i)) addSn addnC exprD exprVn ?mulfK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)