proposition: Fact Tamari_anti : antisymmetric Tamari.
proof: Proof. move=> t1 t2 /andP[/Tamari_sumn_right_sizes [leq21 eq]]. move=> /Tamari_sumn_right_sizes [leq12 _]. by apply/eqP; rewrite -eq eqn_leq leq21 leq12. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype