proposition: Lemma consec2_total ks x1 x2 y1 y2 : uniq ks -> y1 \in ks \/ y2 \in ks -> consec ks x1 y1 -> consec ks x2 y2 -> [|| (x1 == x2) && (y1 == y2), y2 <=[ks] x1 | y1 <=[ks] x2].
proof: Proof. move=>U. suff L a1 a2 b1 b2 : b1 \in ks -> consec ks a1 b1 -> consec ks a2 b2 -> [|| (a1 == a2) && (b1 == b2), b2 <=[ks] a1 | b1 <=[ks] a2]. - case=>Y Cx1 Cx2; first by apply: L. case/or3P: (L _ _ _ _ Y Cx2 Cx1)=>[|->|->]; try by rewrite !orbT. by case/andP=>/eqP/esym -> /eqP/esym ->; rewrite !eq_refl. move=>Y1 Cx1 Cx2; move: (consec_mem Cx1) (consec_mem Cx2)=>X1 X2. case/or3P: (slt_total a2 X1) Cx2 X2=>[/eqP <-{a2}|H|H] Cx2 X2. - by rewrite (consec_next_inj U Y1 Cx1 Cx2) !eq_refl. - by rewrite (consec_next U Cx1 H) !orbT. by rewrite (consec_next U Cx2 H) !orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)