proposition: Lemma consec_indx ks k1 k2 (P : A -> Prop) : uniq ks -> k1 <=[ks] k2 -> k1 \in ks -> P k1 -> (forall t1 t2, t2 \in &=ks `]k1, k2] -> consec (&=ks `[k1, k2]) t1 t2 -> P t1 -> P t2) -> forall t, t \in &=ks `]k1, k2] -> P t.
proof: Proof. move=>U N K H0 IH t; apply: (consec_ind (k:=k1))=>//=. - by rewrite eqslice_uniq // andbT eqslice_mem_uniq //= negb_and in_itv /= ltxx /= orbT. by move=>t1 t2 H C; apply: IH=>//; rewrite eqsl_xxL N /= K. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)