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