proposition: Lemma Tamari_consP v0 v : reflect [/\ v0 <= size v, v \is a TamariVector & forall i, i < v0 -> nth 0 v i + i < v0] (v0 :: v \is a TamariVector).
proof: Proof. rewrite !unfold_in /=. apply (iffP and3P) => [] [Hsz Htam Hall]; split => //. - by move/allP: Hall => H i Hi; apply H; rewrite mem_iota. - by apply/allP => i; rewrite mem_iota /= add0n; exact: Hall. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype