proposition: Lemma lt_absr : forall x y, absr x <<! y -> - y <<! x.
proof: Proof. move=> x y h. have py : 0 <<! y by apply: (ler_ltr_trans (absrpos x)). case: (compareP x 0) => h2. - by rewrite -[x]opprK ltr_oppgtr -[- x]absr_npos // ltrW. - by rewrite -[x]opprK -ltr_oppgtr !opprK; apply: ltr_trans py; rewrite -gtr0_ltNr0. - by rewrite h2 -gtr0_ltNr0. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)