proposition: Lemma remove_min_spec1 s x s' : remove_min s = Some (x,s') -> min_elt s = Some x /\ Equal (remove x s) s'.
proof: Proof. destruct s as (s,Hs). unfold remove_min, mk_opt_t, min_elt, remove, Equal, In; simpl. generalize (fun x s' => @Raw.remove_min_spec1 s x s' Hs). set (P := Raw.remove_min_ok s). clearbody P. destruct (Raw.remove_min s) as [(x0,s0)|]; try easy. intros H [= -> <-]. simpl. destruct (H x s0); auto. subst; intuition. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat