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