proposition: Theorem pred_inj n m : n ~= 0 -> m ~= 0 -> P n == P m -> n == m.
proof: Proof. cases n. - intros H; exfalso; now apply H. - intros n _; cases m. + intros H; exfalso; now apply H. + intros m H2 H3. do 2 rewrite pred_succ in H3. now rewrite H3. Qed.
imports: Decidable NAxioms NZProperties