proposition: Lemma bi_induction (P : Z -> Prop) : Proper (eq ==> iff) P -> P 0 -> (forall x, P x <-> P (succ x)) -> forall z, P z.
proof: Proof. intros _ H0 Hs z. induction z using peano_ind. - assumption. - now apply -> Hs. - apply Hs. now rewrite succ_pred. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass