こんな簡単な証明が分からなかった... まだ使いこなせないな．とりあえずできたからいいか． 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. …