proposition: Lemma split_find m x y `{!Ok m} : find y m = match K.compare y x with | Eq => (split x m)#o | Lt => find y (split x m)#l | Gt => find y (split x m)#r end.
proof: Proof. functional induction (split x m); intros; cleansplit. - now case K.compare. - repeat case K.compare_spec; trivial; order. - simpl in *. rewrite join_find, IHt0; autok. simpl. repeat case K.compare_spec; trivial; order. - rewrite join_find, IHt0; autok. simpl; repeat case K.compare_spec; trivial; order. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)