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