proposition: Theorem max_such_prop : forall (P : nat -> Prop) (P_dec : forall n : nat, {P n} + {~ P n}) (n : nat), (exists x : nat, x <= n /\ P x) -> max_such P P_dec n <= n /\ P (max_such P P_dec n) /\ (forall x : nat, max_such P P_dec n < x -> x <= n -> ~ P x).
proof: Proof. intros P P_dec n; elim n; simpl in |- *; auto. intros (x1, (H1, H2)). case (P_dec 0); auto. intros H3; repeat split; auto; intros x H4 H5; inversion H5; auto. Contradict H5; auto with arith; rewrite H; auto with arith. intros H3; Contradict H2; auto; inversion H1; auto. intros n1 Rec (x1, (H1, H2)); case (P_dec (S n1)); auto. intros H3; repeat split; auto with arith. intros x H H0; (Contradict H0; auto with arith). intros H3; case Rec. exists x1; split; auto with arith. inversion H1; auto. case H3; rewrite <- H; auto. intros H4 (H5, H'5); repeat split; auto. intros x H6 H7; auto. inversion H7; auto with arith. Qed.
imports: Coq(Arith ArithRing)