proposition: Theorem Tamari_vctleq t1 t2 : (right_sizes t1 <=V right_sizes t2) = (t1 <=T t2).
proof: Proof. apply/idP/idP. - have [i] := ubnPleq (sumn (right_sizes t2) - sumn (right_sizes t1)). rewrite leq_subLR. elim: i => [|i IHi] in t1 t2 * => Hsum Hleq. rewrite addn0 in Hsum. suff -> : t1 = t2 by apply: le_refl. apply/val_inj/eqP => /=. have [Hsum2 Heq] := vctleq_sumn_right_sizes Hleq. rewrite -Heq; apply/eqP/anti_leq. by rewrite Hsum Hsum2. case: (t1 =P t2) => [-> | /eqP Hneq]; first by apply: le_refl. have [/= tt [Hrot Htleq]] := vctleq_rotation Hleq Hneq. have Hszt : size_tree tt == n by rewrite (size_rotations Hrot) bintreeszP. pose t := BinTreeSZ Hszt. rewrite -[tt]/(trval t) in Hrot Htleq. have:= sumn_right_sizes_gt Hrot. rewrite -(leq_add2r i) addSnnS => /(leq_trans Hsum). move=> {}/IHi /(_ Htleq) /(le_trans _); apply. by apply: ltW; apply: rotations_Tamari. - rewrite TamariE => /connectP /= [p]. elim: p t1 t2 => /= [| p0 p IHp] t1 t2. by move => _ ->; exact: vctleq_refl. move/andP => [Hrot Hpath Ht2]. suff /vctleq_trans : right_sizes t1 <=V right_sizes p0 by apply; apply IHp. exact: rotations_vctleq_impl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype