proposition: Lemma consec_ind_raw k ks (P : A -> Prop) : k \notin ks -> uniq ks -> P k -> (forall t1 t2, t2 \in ks -> consec (k::ks) t1 t2 -> P t1 -> P t2) -> forall t, t \in k::ks -> P t.
proof: Proof. elim: ks=>[|x ks IH] //= K U H0 Hstep t; first by rewrite inE=>/eqP ->. rewrite inE negb_or in K U; case/andP: K U=>K1 K2 /andP [U1 U2]. rewrite !inE; case/or3P; first by move/eqP=>->. - move/eqP=>->{t}; apply: Hstep H0; first by rewrite inE eq_refl. by rewrite /consec sltL eq_sym K1 (eqsl_oo_split_consec (s1:=[::])). have U : uniq (k::x::ks) by rewrite /= inE negb_or K1 K2 U1 U2. move=>T; apply: IH=>[|||t1 t2 T2 C|] //; last by rewrite inE T orbT. have Nx2 : t2 != x by case: eqP T2 U1=>// ->->. have Nk2 : t2 != k by case: eqP T2 K2=>// ->->. case: (t1 =P k) C=>[->{t1} C _|/eqP Nt1k C]. - suff [Ckx Cxt2] : consec [:: k, x & ks] k x /\ consec [:: k, x & ks] x t2. - have : P x by apply: Hstep Ckx H0; rewrite inE eq_refl. by apply: Hstep Cxt2; rewrite inE T2 orbT. split; first by apply: consec_hd2. apply: consec_cons=>//=. - by rewrite U1. - by rewrite inE negb_or K1. - by rewrite eq_sym. by apply: consec_hdswap C. have Nx1 : t1 != x. - case: eqP U1=>// <-; move: (consec_mem C). by rewrite inE (negbTE Nt1k) /= =>->. apply: Hstep; first by rewrite inE T2 orbT. apply: consec_cons=>//=. - by rewrite U1. - by rewrite inE negb_or K1. by apply: consec_cons=>//; case/consec_behead: C. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)