proposition: Fact TmeetP t t1 t2 : (t <=T Tmeet t1 t2) = (t <=T t1) && (t <=T t2).
proof: Proof. apply/idP/andP => [/le_trans Htr| []]. by split; apply: Htr; first rewrite TmeetC; rewrite TmeetPr. 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: vctminP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype