proposition: Lemma Empty_Node : forall l o r, Empty (Node l o r) <-> o=None /\ Empty l /\ Empty r.
proof: Proof. intros l o r. split. - rewrite Empty_alt. split. + destruct o; auto. generalize (H 1); simpl; auto. + split; rewrite Empty_alt; intros. * generalize (H (xO a)); auto. * generalize (H (xI a)); auto. - intros (H,(H0,H1)). subst. rewrite Empty_alt; intros. destruct a; auto. + simpl; generalize H1; rewrite Empty_alt; auto. + simpl; generalize H0; rewrite Empty_alt; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface