trivial
Require Import
Print
Inductive
Definition
Fixpoint
Lemma
Theorem
Proof
Qed
intro
intros
induction
unfold
fold
apply
simpl
rewrite
reflexivity
case
discriminate
trivial
assumption
（＊＊ Remark 今回はZArithモジュールを使うよ。 Require Import ZArith. をタイプしてね。 ＊） 導入 Coqでは、整数全体の型はZで表され、次のように定義されている。 Coq Z | Zneg : positive -> Z Z0はゼロで、Zposは正の数、Znegは負の数を表している。…
