proposition: Lemma leftcomb_rotations t : leftcomb (size_tree t) \notin rotations t.
proof: Proof. by rewrite rotations_flip flip_leftcomb rightcomb_rotations in_nil. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype