satos---jp/coq_practice_26.v

Created May 18, 2014 13:03

Star () You must be signed in to star a gist
Fork () You must be signed in to fork a gist

Learn more about clone URLs
Clone this repository at <script src="https://gist.github.com/satos---jp/f89d6474d791c1d8cc02.js"></script>
Save satos---jp/f89d6474d791c1d8cc02 to your computer and use it in GitHub Desktop.

Download ZIP

Raw

coq_practice_26.v

	Require Import Arith.
	Goal (221 * 293 * 389 * 397 + 17 = 14 * 119 * 127 * 151 * 313)%nat.
	Proof.
	ring.
	Qed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment