proposition: Lemma Tamari_sumn_right_sizes t1 t2 : Tamari t1 t2 -> sumn (right_sizes t1) <= sumn (right_sizes t2) ?= iff (t1 == t2).
proof: Proof. move/connectP => [] /= p. elim: p t1 t2 => [| t0 p IHp] t1 t2 /=. by move=> _ /= ->; split; rewrite // !eq_refl. move=> /andP[/sumn_right_sizes_gt Hgt {}/IHp /[apply]]. move=> [] /(leq_trans Hgt) Hlt _ {Hgt p t0}. split; first exact: (ltnW Hlt). have:= Hlt; rewrite ltn_neqAle => /andP[/negbTE -> _]. by case: eqP Hlt => [->|] //; rewrite ltnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype