proposition: Lemma Tamari_flip t1 t2 : (flipsz t2 <=T flipsz t1) = (t1 <=T t2).
proof: Proof. suff {t1 t2} Timpl t1 t2 : flipsz t2 <=T flipsz t1 -> t1 <=T t2. apply/idP/idP; first exact: Timpl. by rewrite -{1}(flipszK t1) -{1}(flipszK t2); exact: Timpl. rewrite TamariE => /connectP /= []. case/lastP => [//= _ | p l Hp] /=. move=> /(congr1 (@flipsz n)); rewrite !flipszK => ->. exact: connect0. rewrite last_rcons => Hl; subst l; move: Hp. have /eq_path -> : (fun t t' => trval t' \in rotations t) =2 (fun t t' => trval (flipsz t) \in rotations (flipsz t')). by move=> t t' /=; exact: rotations_flip. rewrite -rev_path /= last_rcons belast_rcons. have -> : rev (flipsz t2 :: p) = [seq flipsz t | t <- rcons [seq flipsz t' | t' <- rev p] t2]. rewrite map_rev -rev_cons map_rev /=. rewrite -map_comp (eq_map (g := id)); last by move=> x /=; rewrite flipszK. by rewrite map_id. rewrite (map_path (b := pred0) (e' := (fun t t' => trval t' \in rotations t))); first last. - by apply/hasP => [] [t /=]. - by rewrite /rel_base => u v _; rewrite /= !flipK. set pp := rcons _ _ => Hp; apply/connectP; exists pp; first by []. by rewrite /pp last_rcons. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype