proposition: Lemma rightcomb_rotationsE t : (rotations t == [::]) = (t == rightcomb (size_tree t)).
proof: Proof. apply/eqP/eqP => [|->]. - elim: t => //= l _ r IHr. case: l => [| ll lr] //= Hrot. have {Hrot} /IHr -> : rotations r = [::] by move: Hrot; case: (rotations r). by rewrite (eqP (size_rightcomb _)). - exact: rightcomb_rotations. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype