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