proposition: Lemma rotations_add_head v0 v t : v0 :: v \is a TamariVector -> (nth 0 v v0 + v0).+1 :: v \is a TamariVector -> from_vct_acc t ((nth 0 v v0 + v0).+1 :: v) \in rotations (from_vct_acc t (v0 :: v)).
proof: Proof. set v1 := nth 0 v v0 => Htam0 Htam1. have {Htam1} Hv1 : (nth 0 v v0 + v0).+1 <= size v. by move/Tamari_consP: Htam1 => []. have Hv0 : v0 < size v by apply: leq_ltn_trans (leq_addl _ _) Hv1. have -> : v = (take v0 v) ++ v1 :: (take v1 (drop v0.+1 v)) ++ (drop (v1 + v0.+1) v). rewrite -drop_drop cat_take_drop. rewrite -{1}(cat_take_drop v0 v); congr (_ ++ _). rewrite -add1n -drop_drop drop1. have -> : v1 = head 0 (drop v0 v) by rewrite -nth0 nth_drop addn0. apply/esym/cons_head_behead. by apply/eqP/nilP; rewrite /nilp size_drop subn_eq0 -ltnNge. have szvl : size (take v0 v) = v0 by rewrite size_take Hv0. have szvm : size (take v1 (drop v0.+1 v)) = v1. rewrite size_takel // size_drop. by move: Hv1 => /(leq_sub2r v0.+1); rewrite subSS addnK. rewrite /from_vct !from_vct_accE. rewrite !drop_cat !take_cat szvl ltnn subnn drop0 cats0. rewrite -addSn ltnNge leq_addl /= addnK /=. rewrite from_vct_accE !take_cat szvm ltnn subnn take0 cats0. rewrite drop_cat szvm ltnn subnn drop0. have {Htam0} Htam := Tamari_take Htam0. rewrite (from_vct_cat _ _ Htam) from_vct_accE. rewrite -{1 3}szvm take_size drop_size from_vct_acc_nil. rewrite from_vct_cat_leftE [X in rotations X]from_vct_cat_leftE. apply catleft_rotations. move: (from_vct_acc _ (take v0 _)) => tb. move: (from_vct_acc _ (take v1 _)) => tc. by apply/rotationP; exists t, tb, tc; exact: Or31. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype