proposition: Lemma right_sizes_meet t1 t2 : right_sizes (t1 /\T t2) = vctmin (right_sizes t1) (right_sizes t2).
proof: Proof. rewrite /Order.meet /= from_vctK // vctmin_Tamari //. by rewrite !size_right_sizes !bintreeszP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype