proposition: Lemma remove_min_spec2 s : remove_min s = None -> Empty s.
proof: Proof. destruct s as (s,Hs). unfold remove_min, mk_opt_t, Empty, In; simpl. generalize (Raw.remove_min_spec2 s). set (P := Raw.remove_min_ok s). clearbody P. destruct (Raw.remove_min s) as [(x0,s0)|]; now intuition. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat