proposition: Lemma consec_rconsEP' k k1 k2 ks : uniq ks -> k \notin ks -> consec (rcons ks k) k1 k2 <-> if k1 != k then if k2 \notin ks then k2 = k /\ exists ks', ks = rcons ks' k1 else consec ks k1 k2 else k2 \notin rcons ks k.
proof: Proof. move=>U K; split; last first. - case: eqP=>[-> /= K2|/eqP N /=]. - by apply/consecP_last=>//; [rewrite rcons_uniq K U | exists ks]. case: ifP=>K2; last first. - move/negbT: K2; rewrite negbK=>K2 /(consecP_inlt _ _ U) [K1 E]. apply/consecP_inlt; first by rewrite rcons_uniq K. split; first by rewrite mem_rcons inE K1 orbT. move=>z; rewrite mem_rcons inE; case/orP=>[/eqP ->{z}|Z]. - rewrite slt_rcons K2 sle_rcons (negbTE K) eq_refl andbT K1 /=. by apply/negP=>/slt_memE; rewrite (negbTE K). by rewrite slt_rcons K2 sle_rcons Z; apply: E. case=>->{k2 K2} [ks' E]; rewrite {ks}E in U K *. apply/consecP_inlt; first by rewrite rcons_uniq K. split. - by rewrite mem_rcons inE mem_rcons inE eq_refl orbT. rewrite rcons_uniq in U; case/andP: U=>N1 U. rewrite mem_rcons inE negb_or eq_sym N /= in K. move=>z; rewrite mem_rcons inE mem_rcons inE => Z. rewrite slt_rcons mem_rcons inE eq_sym (negbTE N) (negbTE K) /=. rewrite eq_refl orbF !sle_rcons N1 /= eq_refl orbF !mem_rcons !inE eq_refl /=. case: eqP Z=>[->{z} /= _|/eqP Nz /=]. - by rewrite eq_sym (negbTE N) /=; case: ifP=>// K'; rewrite K' sle_memI. rewrite (eq_sym z); case: eqP=>[/= ->|/=]; first by rewrite sle_refl if_same. by move=>_ Z; rewrite Z sle_memI. case/consecP_inlt; first by rewrite rcons_uniq K. move=>+ E; rewrite mem_rcons inE=>K1. case/orP: K1 E=>[/eqP ->{k1}|K1] E. - rewrite eq_refl /=. move: (E k); rewrite mem_rcons inE eq_refl=>/(_ erefl). rewrite sle_refl; apply: contraL; rewrite mem_rcons inE. case/orP=>[/eqP ->|K2]; first by rewrite slt_irr. rewrite slt_rcons K2; apply/negP. by move/(slt_trans (slt_memI K2 K)); rewrite slt_irr. case: eqP K1 K=>[->->//|/eqP N K1 K /=]; case: ifP=>K2; last first. - move/negbT: K2; rewrite negbK=>K2; apply/consecP_inlt=>//. split=>// z Z; move: (E z); rewrite mem_rcons inE Z orbT=>/(_ erefl). by rewrite slt_rcons K2 sle_rcons Z. move: (E k); rewrite mem_rcons inE eq_refl=>/(_ erefl). rewrite slt_rcons (negbTE K2) (negbTE K) /= eq_refl andbT. rewrite sle_rcons (negbTE K) K1 /=; case: eqP=>// -> _; split=>//. suff -> : k1 = last k1 ks. - move: ks {E N U K K2} k1 K1; apply: last_ind=>[//|ks x IH] k1. rewrite mem_rcons inE; case/orP=>[/eqP ->|]. - by rewrite last_rcons; exists ks. by case/IH=>ks' E; rewrite last_rcons; exists ks. apply/eqP/contraT; rewrite eq_sym=>M; exfalso. move: (last_change M)=>L. move: (E (last k1 ks)); rewrite mem_rcons inE L orbT=>/(_ erefl). rewrite slt_rcons sle_rcons (negbTE K2) L /=. move/esym; rewrite sle_eqVlt; last by rewrite L. rewrite (negbTE M) /=. by move/(sle_slt_trans (sle_last k1 U K1)); rewrite slt_irr. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)