Induction on propositionally proof-irrelevant naturals

prop_nat.v

Require Import Coq.Program.Tactics.
Require Import Coq.Unicode.Utf8.
Require Import Coq.Logic.ProofIrrelevance.

Module prop_nat.
  Inductive N : Prop := Z : N | S : N -> N.

  (* Auto-generated. *)
  Fixpoint N_ind' {P : Prop} (z : P) (s : N -> P -> P) (n : N) : P :=
    match n with
    | Z => z
    | S n0 => s n0 (N_ind' z s n0)
    end.

  Fixpoint N_ind'' {P : N -> Prop} (z : P Z) (s : ∀ n : N, P n -> P (S n)) (n : N) : P n :=
    match n with
    | Z => z
    | S n0 => s n0 (N_ind'' z s n0)
    end.

  Lemma N_irr (n1 n2 : N) : n1 = n2.
  Proof. apply proof_irrelevance. Qed.
End prop_nat.