Skip to content

Instantly share code, notes, and snippets.

@vhxs

vhxs/rings-example-in-coq.v

Last active August 31, 2022 22:46
Show Gist options
  • Save vhxs/83fff8d089068e614d2441d9d97e641f to your computer and use it in GitHub Desktop.
Save vhxs/83fff8d089068e614d2441d9d97e641f to your computer and use it in GitHub Desktop.
Download ZIP
Raw
rings-example-in-coq.v
(* Coq is a proof assistant. Not a theorem prover. *)
(* also github has syntax highlighting for Coq, wow. *)
Require Import Ring.
Require Import Arith.
Theorem simply_poly : forall (x : nat), (x + 1) * (x + 2) = x * x + 3 * x + 2.
Proof. intros. ring. Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment