proposition: Lemma TmeetPr t1 t2 : Tmeet t1 t2 <=T t2.
proof: Proof. have Hszeq : size (right_sizes t1) = size (right_sizes t2). by rewrite !size_right_sizes !bintreeszP. rewrite /Tmeet -Tamari_vctleq /= from_vctK ?vctmin_Tamari //. exact: vctminPr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype