proposition: Lemma rotationP t1 t2 : reflect (exists a b c, [\/ [/\ t1 = BinNode (BinNode a b) c & t2 = BinNode a (BinNode b c)], [/\ t1 = BinNode a c, t2 = BinNode b c & b \in rotations a] | [/\ t1 = BinNode a b, t2 = BinNode a c & c \in rotations b]]) (t2 \in rotations t1).
proof: Proof. apply (iffP idP) => [|]. - case Ht1 : t1 => [//|[|a b] c]. rewrite /= => /mapP /= [rc Hrc ->]. by exists BinLeaf, c, rc; apply Or33. rewrite [X in X -> _]/= inE => /orP[/eqP->{t2}|]. by exists a, b, c; apply Or31. rewrite mem_cat => /orP[/mapP[lrot] | /mapP[rrot Hrrot ->]]. + rewrite -[lrot \in _]/(lrot \in rotations (BinNode a b)) => Hlrot ->. by exists (BinNode a b), lrot, c; apply Or32. + by exists (BinNode a b), c, rrot; apply Or33. - move=> [a] [b] [c] [] [-> ->]. + by rewrite inE eq_refl. + exact: rotations_left_sub. + exact: rotations_right_sub. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype