proposition: Theorem find_min_correct : forall l : list A, match find_min l with | None => l = [] | Some (a, b) => (In b l /\ a = f b) /\ (forall c : A, In c l -> f b <= f c) end.
proof: Proof. intros l; elim l; simpl in |- *; auto. intros a l0; case (find_min l0); simpl in |- *. intros p; case p; simpl in |- *. intros n b ((H1, H2), H3); case (le_lt_dec n (f a)); simpl in |- *. intros H4; split; auto. intros c [H5| H5]; auto. rewrite <- H2; rewrite <- H5; auto. intros H4; split; auto. intros c [H5| H5]; auto. rewrite <- H5; auto. apply Nat.le_trans with (f b); auto. rewrite <- H2; auto with arith. intros H; rewrite H; split; simpl in |- *; auto. intros c [H1| H1]; rewrite H1 || case H1; auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)