proposition: Lemma add_spec1 m x e `{!Ok m} : find x (add x e m) = Some e.
proof: Proof. functional induction (add x e m); simpl; intros; cleanf; trivial. - now rewrite F.compare_refl. - invok. rewrite bal_find; autok. simpl. case K.compare_spec; try order; auto. - invok. rewrite bal_find; autok. simpl. case K.compare_spec; try order; auto. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)