false_beq_nat (ソフトウェアの基礎、Coq)のメモ

Coqの帰納法を忘れかけてたのでメモ

(** **** Exercise: 2 stars (false_beq_nat)  *)
Theorem false_beq_nat : forall n m : nat,
     n <> m ->
     beq_nat n m = false.
Proof.
  intros n.
  unfold not.
  induction n as [ | n'].
    - intros m H (**ここでmをintros**). destruct m as [ | n'].
                 * apply ex_falso_quodlibet. apply H. reflexivity.
                 * simpl. reflexivity.
    - intros m H (**ここでmをintros**). destruct m as [ | m'].
                 * simpl. reflexivity.
                 * simpl. apply IHn'. intros H1. apply H. rewrite -> H1. reflexivity. Qed.