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