proposition: Lemma add_find m x y e `{!Ok m} : find y (add x e m) = match K.compare y x with Eq => Some e | _ => find y m end.
proof: Proof. case K.compare_spec; intros E. - apply find_spec; autok. rewrite E. apply find_spec; autok. now apply add_spec1. - apply add_spec2; trivial; order. - apply add_spec2; trivial; order. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)