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