proposition: Lemma size_rotations t t' : t' \in rotations t -> size_tree t' = size_tree t.
proof: Proof. elim: t t' => //= l IHl r IHr t' /=. case H: l => [| ll lr] //; first by move/mapP => [/= lrot /IHr <- ->]. rewrite inE=> /orP[/eqP->|]; first by rewrite /= !(add1n, addSn, addnS) addnA. by rewrite -H mem_cat => /orP[/mapP/=[lrot /IHl] | /mapP/=[rrot /IHr]] <- ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype