proposition: Lemma ltrW : forall x y, x <<! y -> x <<= y .
proof: Proof. Proof . by move=> x y H; rewrite ler_ltreq H . Qed . Lemma lerNgtr : forall x y, (x <<= y) = ~~ (y <<! x). Proof. move=> x y; rewrite ltr_lerne eq_ler; case e: (y <<= x); rewrite ?negbK //=. by move: (ler_total x y); rewrite e orbF. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)