Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503

yoshihiro503/le_Sn_n.v

Created February 23, 2013 07:31
Show Gist options
  • Save yoshihiro503/5018836 to your computer and use it in GitHub Desktop.
Save yoshihiro503/5018836 to your computer and use it in GitHub Desktop.
Download ZIP
「ソフトウェアの基礎」 Rel_Jの練習問題 le_Sn_n の形式的な証明 http://proofcafe.org/sf/Rel_J.html
Raw
le_Sn_n.v
(** **** 練習問題:★, optional *)
Theorem le_Sn_n : forall n,
~ (S n <= n).
Proof.
intro n. intro H. induction n.
inversion H.
apply IHn. apply le_S_n. apply H.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment