Coqで証明書いてみた
Require Import Arith.
Theorem Th1 :
forall (n : nat),
(exists m : nat, n = m * 2)
-> exists k : nat, n * 2 = k * 4.
Proof.
intros.
destruct H.
exists x.
rewrite H.
rewrite mult_assoc_reverse.
simpl.
reflexivity.
Qed.
Author And Source
この問題について(Coqで証明書いてみた), 我々は、より多くの情報をここで見つけました https://qiita.com/Thought_Nibbler/items/9ed7da5ecfa046c8f9f5著者帰属：元の著者の情報は、元のURLに含まれています。著作権は原作者に属する。
Content is automatically searched and collected through network algorithms . If there is a violation . Please contact us . We will adjust (correct author information ,or delete content ) as soon as possible .