proposition: Lemma catleft_rotations t t1 t2 : t1 \in rotations t2 -> (cat_left t t1) \in rotations (cat_left t t2).
proof: Proof. elim: t => [| tl IHtl tr _]; first by rewrite !cat_left0t. move=> {}/IHtl Hrec. apply/rotationP; exists (cat_left tl t2), (cat_left tl t1), tr. by apply Or32. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype