proposition: Lemma ltrN : forall x y, x <<! y -> ~~ (y <<! x).
proof: Proof. by move=> x y; case e: (y <<! x) => //; move/(ltr_trans e); rewrite ltr_irrefl. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)