proposition: Lemma vct_succ u v0 v w : w \is a TamariVector -> u ++ v0 :: v <=V w -> w <=V u ++ (nth 0 v v0 + v0).+1 :: v -> w = u ++ v0 :: v \/ w = u ++ (nth 0 v v0 + v0).+1 :: v.
proof: Proof. move=> Htamw Hvw Hwv0. case: (w =P u ++ v0 :: v) => [Heq | Hneq]; first by left. right; pose w0 := nth 0 w (size u). have Hw : w = u ++ w0 :: v. have Hsz : size w = (size u + size v).+1. by move: Hvw => /vctleqP[<- _]; rewrite !size_cat /= addnS. apply (eq_from_nth (x0 := 0)); first by rewrite Hsz size_cat /= addnS. move=> i; rewrite Hsz ltnS => Hi. case: (ltngtP i (size u)) => [Hiu | Hui | ->]. - rewrite nth_cat Hiu; apply/anti_leq/andP; split. + by move/vctleqP: Hwv0 => [_ /(_ i)]; rewrite nth_cat Hiu. + by move/vctleqP: Hvw => [_ /(_ i)]; rewrite nth_cat Hiu. - have Hf : i < size u = false by rewrite ltnNge (ltnW Hui). rewrite nth_cat Hf. have:= Hui; rewrite -subn_gt0; case Hd : (i - size u) => [| d] //= _. apply/anti_leq/andP; split. + by move/vctleqP: Hwv0 => [_ /(_ i)]; rewrite nth_cat Hf Hd. + by move/vctleqP: Hvw => [_ /(_ i)]; rewrite nth_cat Hf Hd. + by rewrite nth_cat ltnn subnn. rewrite Hw; suff -> : w0 = (nth 0 v v0 + v0).+1 by []. apply/anti_leq/andP; split. - by move/vctleqP: Hwv0 => [_ /(_ (size u))]; rewrite Hw !nth_cat ltnn subnn. - have Hv0w0 : v0 < w0. rewrite ltn_neqAle; apply/andP; split. + by move: Hneq; apply contra_notN; rewrite Hw => /eqP ->. + by move/vctleqP: Hvw => [_ /(_ (size u))]; rewrite Hw !nth_cat ltnn subnn. - by rewrite Hw in Htamw Hvw; exact: (Tamari_add_min Htamw). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype