proposition: Lemma rotations_right_sub l r1 r2 : r1 \in rotations r2 -> BinNode l r1 \in rotations (BinNode l r2).
proof: Proof. case Hl : l => [/= |ll lr] H; first by apply/mapP; exists r1. rewrite -Hl /= {2}Hl. rewrite inE; apply/orP; right. rewrite mem_cat; apply/orP; right. by apply/mapP; exists r1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype