Search code examples
coq

Using eq_refl to get an "x = x" hypothesis

In short, is this possible?

I'm trying to prove that cancellation works in a group.

I have 

a, b, x : G
H: a <+> x = b <+> x

and I would like to prove

a = b

My idea was to get a hypothesis

H2: a <+> x <+> i x = a <+> x <+> i x

(i is the inverse function).

I have tried 

pose proof eq_refl (a <+> x <+> i x) as H.

but this does not seem to work.

Solution

  • If your goal really looks like what you posted, then your tactic should fail because it is reusing the name H. If this is not the problem, then it would help to know what error message Coq displays.