fact: Fixpoint max_such (P : nat -> Prop) (P_dec : forall n : nat, {P n} + {~ P n}) (n : nat) {struct n} : nat := match P_dec n with | left _ => n | right _ => match n with | O => 0 | S n1 => max_such P P_dec n1 end end.
imports: Coq(Arith ArithRing)