proposition: Lemma remove_min_spec1 s x s' `{Ok s}: remove_min s = Some (x,s') -> min_elt s = Some x /\ remove x s = s'.
proof: Proof. unfold remove_min. destruct s as [|c l y r]; try easy. generalize (delmin_spec l y r c). destruct delmin as (x0,s0). intros D. destruct (D x0 s0) as (->,<-); auto. fold (remove x0 (Node c l y r)). inversion_clear 1; auto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat