proposition: Theorem bi_induction : forall n, A n.
proof: Proof. intro n. setoid_replace n with (ZnZ.of_Z (ZnZ.to_Z n)). - apply B_holds. apply ZnZ.spec_to_Z. - red. symmetry. apply ZnZ.of_Z_correct. apply ZnZ.spec_to_Z. Qed.
imports: NZAxioms ZArith Zpow_facts DoubleType CyclicAxioms Lia