proposition: Lemma invrN1 : (-1)^-1 = -1 :> R.
proof: Proof. by rewrite -{2}(divrr unitrN1) mulN1r opprK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)