proposition: Lemma TamariP v : reflect ((forall i, i < size v -> nth 0 v i + i < size v) /\ (forall i j, i < j <= nth 0 v i + i -> nth 0 v j + j <= nth 0 v i + i)) (v \is a TamariVector).
proof: Proof. apply (iffP idP); elim: v => [_ | v0 v IHv ] //=. by split => // i j; rewrite !nth_nil => /andP[_]; rewrite !add0n. - move/Tamari_consP => [Hv0 {}/IHv [Hrec1 Hrec2] H]; split. + case=> [_ |i]; rewrite !ltnS /= ?addn0 // addnS; exact: Hrec1. + case=> [//=| i] [//=| j] /=. by rewrite !addnS !addn0 ; exact: H. by rewrite !addnS !ltnS; exact: Hrec2. - move=> [H1 H2]. apply/Tamari_consP; split. + by have:= H1 0 (ltn0Sn _); rewrite addn0 ltnS. + apply: IHv; split => [i Hi | i j Hij]. * by have:= H1 i.+1 Hi; rewrite /= addnS ltnS. * by have:= H2 i.+1 j.+1; rewrite /= !addnS !ltnS; apply. + move=> i Hi. by have:= H2 0 i.+1; rewrite /= !addn0 addnS; apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype