proposition: Lemma invrN x : (- x)^-1 = - x^-1.
proof: Proof. have [Ux | U'x] := boolP (x \is a unit); last by rewrite !invr_out ?unitrN. by rewrite -mulN1r invrM ?unitrN1 // invrN1 mulrN1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)