proposition: Theorem bi_induction : forall A : N -> Prop, Proper (Logic.eq==>iff) A -> A 0 -> (forall n, A n <-> A (succ n)) -> forall n : N, A n.
proof: Proof. intros A A_wd A0 AS. apply peano_rect. - assumption. - intros; now apply -> AS. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties