proposition: Lemma delmin_spec l y r c x s' `{O : Ok (Node c l y r)} : delmin l y r = (x,s') -> min_elt (Node c l y r) = Some x /\ del x (Node c l y r) = s'.
proof: Proof. revert y r c x s' O. induction l as [|lc ll IH ly lr _]. - simpl. intros y r _ x s' _. injection 1; intros; subst. now rewrite MX.compare_refl. - intros y r c x s' O. simpl delmin. specialize (IH ly lr). destruct delmin as (x0,s0). destruct (IH lc x0 s0); clear IH; [ok|trivial|]. remember (Node lc ll ly lr) as l. simpl min_elt in *. intros E. replace x0 with x in * by (destruct lc; now injection E). split. * subst l; intuition. * assert (X.lt x y). { inversion_clear O. assert (InT x l) by now apply min_elt_spec1. auto. } simpl. case X.compare_spec; try order. destruct lc; injection E; subst l s0; auto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat