proposition: Lemma bi_induction_pred : forall A : t -> Prop, Proper (eq==>iff) A -> A 0 -> (forall n, A n -> A (S n)) -> (forall n, A n -> A (P n)) -> forall n, A n.
proof: Proof. intros. apply bi_induction; auto. clear n. intros n; split; auto. intros G; apply H2 in G. rewrite pred_succ in G; auto. Qed.
imports: NumPrelude NZAxioms NZBase NZOrder NZAddOrder PeanoNat