proposition: Fact leftcomb_bottom t : leftcombsz n <=T t.
proof: Proof. rewrite -Tamari_vctleq right_sizes_left_comb. apply/vctleqP; split; first by rewrite size_nseq size_right_sizes bintreeszP. by move=> i; rewrite nth_nseq if_same. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype