proposition: Lemma RemoveMin_step l x e r h m' p : RemoveMin (Node h l x e r) (m',p) -> (l = Leaf _ /\ m' = r /\ p = (x,e) \/ exists m0, RemoveMin l (m0,p) /\ m' = bal m0 x e r).
proof: Proof. simpl. destruct l as [|lh ll lx le lr]; simpl. - intros [= <- <-]. now left. - destruct (remove_min ll lx le lr) as (l',p'). intros [= <- <-]. right. now exists l'. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)