proposition: Theorem right_sizesP t : right_sizes t \is a TamariVector.
proof: Proof. have [n] := ubnP (size_tree t); elim: n => // n IHn in t * => /ltnSE-leszt. rewrite -(left_branchK t) right_sizes_from_left. have : all (fun t => size_tree t < n) (rev (left_branch t)). rewrite all_rev; have:= size_left_branch t. by apply sub_all => l Hl; apply: leq_trans Hl leszt. elim: (rev (left_branch t)) => [| b0 br IHbr] //=. move=> /andP[{}/IHn Hb0 {}/IHbr Hbr]. rewrite -/((_ :: _) ++ _); apply Tamari_cat; last exact: Hbr. by rewrite -size_right_sizes; exact: cons_TamariP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype