proposition: Lemma pi_inv : {morph \pi_{alg F} : x / inv_algcreal x >-> inv_alg x}.
proof: Proof. unlock inv_alg=> x; symmetry; rewrite -equiv_alg /= /inv_algcreal. case: eq_algcreal_dec=> /= [|x'_neq0]. by rewrite pi_algK; case: eq_algcreal_dec. move: x'_neq0 (x'_neq0); rewrite {1}pi_algK. case: eq_algcreal_dec=> // x'_neq0' x_neq0 x'_neq0 /=. by apply: eq_creal_inv; rewrite pi_algK. Qed.
imports: HB(structures) 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 generic_quotient) mathcomp(cauchyreals separable zmodp bigenough)