proposition: Lemma invr1_0ltr_ltrI1 : forall x, x <<! 0 -> (-1 <<! x) = (x^-1 <<! -1).
proof: Proof. move=> x; rewrite -(opprK x). rewrite invrN !ltr_oppgtr -lt0r_gtNr0 opprK; exact: invr1_ltr0_ltr1. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)