proposition: Lemma Tamari_succ t1 t2 t : trval t2 \in rotations t1 -> t1 <=T t -> t <=T t2 -> t = t1 \/ t = t2.
proof: Proof. move/rotations_right_sizesP => [u] [v0] [v] [Ht1 Ht2]. move: (right_sizesP t); rewrite -!Tamari_vctleq Ht1 Ht2 => Htam H1 H2. have [] := vct_succ Htam H1 H2. - rewrite -Ht1 => /(congr1 from_vct); rewrite !right_sizesK => Heq. by left; apply val_inj. - rewrite -Ht2 => /(congr1 from_vct); rewrite !right_sizesK => Heq. by right; apply val_inj. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype