こんな簡単な証明が分からなかった... まだ使いこなせないな．とりあえずできたからいいか． Require Import Arith.Lemma ge1andlt2 : forall n:nat, 1 <= n < 2 -> n = 1. Proof. intros n H. elim H. intros Hge Hlt. assert (1 <= n <= 1). constructor. …

ProofGeneral で Coq を使う．Coq のインストール方法はハイテンションなインストール記事にまかせるとします． この記事みたいにハイテンションにインストール記事を書こうかとも思ったけどレベルが高すぎます． Mac にウインドウズ・ベロは無いしw Mac 版…