proposition: Lemma ler_opp_ler0 : forall x, ( x <<= -x) = (x <<= 0).
proof: Proof. move=> x;rewrite -(lerTlb x) addNr. case e : (x <<= 0); first by rewrite ler0T //. by apply: negbTE; rewrite lerNgtr negbK ltrT0 // ltrNger e. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)