proposition: Lemma covers_Tamari t1 t2 : (trval t2 \in rotations t1) = (covers t1 t2).
proof: Proof. apply/idP/coversP => [Hrot|]. - split => /= [|z /andP[H1 H2]]; first exact: rotations_Tamari. have [HA1|HA2] := Tamari_succ Hrot (ltW H1) (ltW H2). + by move: H1; rewrite HA1 ltxx. + by move: H2; rewrite HA2 ltxx. - rewrite lt_def => [[/andP[neq le12 Hcov]]]. move: le12; rewrite TamariE => /connectP[/= [|s0 [|s1 s]] /= Hpath Ht2]. + by rewrite Ht2 eqxx in neq. + by move: Hpath; rewrite andbT Ht2. + move: Hpath => /and3P[Hs0 Hs1 Hpath]; exfalso; apply: (Hcov s0). rewrite (rotations_Tamari Hs0) /=. apply: (lt_le_trans (rotations_Tamari Hs1)). by rewrite TamariE; apply/connectP; exists s. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype