1 <= n < 2 ならば n = 1

Coq

こんな簡単な証明が分からなかった...
まだ使いこなせないな．

とりあえずできたからいいか．



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.

  apply Hge.

  apply lt_n_Sm_le.

  apply Hlt.

  elim H0.

  intros.

  apply le_antisym.

  apply H2.

  apply H1.

Qed.

もっと簡単に解ける気がするけど．
ポイントは n = 1 と 1 <= n <= 1 が等価であること．
これに気付くのに貴重な盆休みがぁぁぁ．