proposition: Lemma consecP ks t1 t2 : reflect (t1 <[ks] t2 /\ ~~ has predT (&=ks `]t1, t2[)) (consec ks t1 t2).
proof: Proof. apply: (iffP andP); case=>-> H; split=>//. - by rewrite -nilp_hasPn. by rewrite nilp_hasPn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)