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