proposition: Lemma rotations_Tamari t t' : trval t' \in rotations t -> t <T t'.
proof: Proof. move=> H; rewrite lt_def eq_sym rotations_neq //=. exact: connect1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype