Skip to content

Instantly share code, notes, and snippets.

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

What would you like to do?
(* Original version of the proof in *)
Theorem square_is_unique (G : group) :
forall (f : G), f <.> f = f -> f = id.
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.
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.