proposition: Lemma mul_Valg (x : alg) : x != zero_alg -> mul_alg (inv_alg x) x = one_alg.
proof: Proof. elim/quotW: x=> x; rewrite piE -(rwP neq_algcrealP) /= => x_neq0. apply/eqP; rewrite piE; apply/eq_algcrealP; rewrite /= /inv_algcreal. case: eq_algcreal_dec=> [/(_ x_neq0) //|/= x_neq0']. apply: eq_crealP; exists_big_modulus m F. by move=> * /=; rewrite mulVf ?subrr ?normr0 ?creal_neq0_always. by close. 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)