proposition: Lemma rotations_left_sub l1 l2 r : l1 \in rotations l2 -> BinNode l1 r \in rotations (BinNode l2 r).
proof: Proof. case H2 : l2 => [/= |ll2 lr2]; first by rewrite in_nil. rewrite -H2 /= {2}H2 => Hin. rewrite inE; apply/orP; right. rewrite mem_cat; apply/orP; left. by apply/mapP; exists l1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype