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.
More than 5 years have passed since last update.
Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme
List of users who liked
32