proposition: Theorem bi_induction : forall n, A n.
proof: Proof. intro n. setoid_replace n with (N_of_Z (to_Z n)). apply B_holds. apply spec_pos. red. now rewrite spec_N_of_Z by apply spec_pos. Qed.
imports: ZArith OrdersFacts Nnat NAxioms NSig Lia