proposition: Lemma sym_divring : divring_closed (symmetric (n := n) (R := R)).
proof: Proof. split; try solve [apply/rpred1 | apply/rpredB]. move=> p q sym_p sym_q /=; case: (boolP (q \isn't a GRing.unit)). by move/invr_out=> ->; apply/rpredM. rewrite negbK=> inv_q; apply/(msymMK _ sym_q). by apply/contraTneq: inv_q=> ->; rewrite unitr0. by rewrite mulrCA divrr // mulr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg