集合論に基づいた言語を作りたいat TECH
集合論に基づいた言語を作りたい - 暇つぶし2ch841:片山博文MZ ◆T6xkBnTXz7B0
15/01/21 22:08:31.55 OPHJ2hAi.net
>>840
Require Import Arith.
Theorem t: forall n:nat, 2*n = n+n.
intros.
replace (n+n) with (1*n + 1*n).
replace 2 with (1+1).
apply mult_plus_distr_r.
auto.
replace (1*n) with n.
auto.
symmetry.
apply mult_1_l.
Qed.


次ページ
最新レス表示
レスジャンプ
類似スレ一覧
スレッドの検索
話題のニュース
おまかせリスト
オプション
しおりを挟む
スレッドに書込
スレッドの一覧
暇つぶし2ch