kobayashi_qa.v

Require Import Arith Unicode.Utf8.

Definition f (n : nat) :=
  n - 1.

Inductive reaches_1 : nat → Prop :=
  | term_done : reaches_1 1
  | term_more (n : nat) : reaches_1 (f n) → reaches_1 n.

Check reaches_1_ind.

Theorem a01 : ∀ n, n <> 0 -> reaches_1 n.
Proof.
  induction n; [now auto | intros _].
  destruct n; [now apply term_done | apply term_more].
  unfold f. simpl.
  apply IHn.
  now apply Nat.neq_succ_0.
Qed.

Theorem not_reaches_1_0_aux : forall n, n=0 -> ~ reaches_1 n.
Proof.
  intros n n0 rn.
  induction rn; [now auto |].
  apply IHrn. unfold f. now rewrite n0.
Qed.

Theorem not_reaches_1_0 : ~ reaches_1 0.
Proof.
  now apply (not_reaches_1_0_aux 0).
Qed.