proposition: Lemma Tmeet_proof t1 t2 : size_tree (from_vct (vctmin (right_sizes t1) (right_sizes t2))) == n.
proof: Proof. by rewrite size_from_vct size_vctmin !size_right_sizes !bintreeszP minnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype