proposition: Lemma central_induction_pred : forall A : t -> Prop, Proper (eq==>iff) A -> forall n0, A n0 -> (forall n, A n -> A (S n)) -> (forall n, A n -> A (P n)) -> forall n, A n.
proof: Proof. intros. assert (A 0). - destruct (itersucc_or_iterpred 0 n0) as (k,[Hk|Hk]); rewrite Hk; clear Hk. + clear H2. induction k; simpl in *; auto. + clear H1. induction k; simpl in *; auto. - apply bi_induction_pred; auto. Qed.
imports: NumPrelude NZAxioms NZBase NZOrder NZAddOrder PeanoNat