Skip to content

Instantly share code, notes, and snippets.

@miikka miikka/square.v Secret
Created Feb 27, 2016

Embed
What would you like to do?
(* 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
You can’t perform that action at this time.