Skip to content

Instantly share code, notes, and snippets.

@miikka

miikka/square.v Secret

Created February 27, 2016 10:04
Show Gist options
  • Save miikka/8c1c9df08115dfe56f4f to your computer and use it in GitHub Desktop.
Save miikka/8c1c9df08115dfe56f4f to your computer and use it in GitHub Desktop.
Download ZIP
Raw
square.v
(* Original version of the proof in
https://quanttype.net/posts/2016-02-16-elementary-algebra.html *)
Theorem square_is_unique (G : group) :
forall (f : G), f <.> f = f -> f = id.
Proof.
intros f H1.
assert ((inv f) <.> (f <.> f) = (inv f) <.> f) as H2.
- f_equal. assumption.
- rewrite op_assoc, <- op_inv_l, <- op_id_l in H2.
assumption.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment