proposition: Lemma compare_empty_x: forall a, is_empty a = true -> forall b, compare a b = if is_empty b then Eq else Lt.
proof: Proof. induction a as [|l IHl o r IHr]; trivial. destruct o. - intro; discriminate. - simpl is_empty. rewrite <- andb_lazy_alt, andb_true_iff. intros [Hl Hr]. destruct b as [|l' [|] r']; simpl compare; trivial. + rewrite Hl, Hr. trivial. + rewrite (IHl Hl), (IHr Hr). simpl. case (is_empty l'); case (is_empty r'); trivial. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface