proposition: Lemma remove_min_ok (s:t) `{Ok s}: match remove_min s with | Some (_,s') => Ok s' | None => True end.
proof: Proof. generalize (remove_min_spec1 s). destruct remove_min as [(x0,s0)|]; auto. intros R. destruct (R x0 s0); auto. subst s0. auto_tc. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat