proposition: Theorem neq_succ_0 : forall n, S n ~= 0.
proof: Proof. intros n EQ. assert (EQ' := pred_succ n). rewrite EQ, pred_0 in EQ'. rewrite <- EQ' in EQ. now apply (neq_succ_diag_l 0). Qed.
imports: Decidable NAxioms NZProperties