proposition: Lemma ins_find m x y v `{!Ok m} : find y (ins x v m) = match K.compare y x with Eq => Some v | _ => find y m end.
proof: Proof. destmatch; intros E. - apply find_spec; autok. rewrite E. apply find_spec; autok. now apply ins_spec1. - apply ins_spec2; trivial; order. - apply ins_spec2; trivial; order. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)