Coq: Недостаточная ошибка ошибки

Question

Я новичок в Coq и получаю ошибку Insufficient Justification для гипотезы H3. Я пробовал переписывать его несколько раз, но ошибка сохраняется. Может кто-нибудь объяснить, почему? Благодарю.

Section GroupTheory. 
Variable G: Set. 
Variable operation: G -> G -> G. 
Variable e : G. 
Variable inv : G -> G. 
Infix "*" := operation. 

Hypothesis associativity : forall x y z : G, (x * y) * z = x * (y * z). 
Hypothesis identity : forall x : G, exists e : G, (x * e = x) /\ (e * x = x). 
Hypothesis inverse : forall x : G, (x * inv x = e) /\ (inv x * x = e). 

Theorem latin_square_property : 
    forall a b : G, exists x : G, a * x = b. 
proof. 
    let a : G, b : G. 
    take (inv a * b). 
    have H1:(a * (inv a * b) = (a * inv a) * b) by associativity. 
    have H2:(a * inv a = e) by inverse. 
    have H3:(e * b = b) by identity. 
    have (a * (inv a * b) = (a * inv a) * b) by H1. 
         ~= (e * b) by H2. 
         ~= (b) by H3. 
hence thesis. 
end proof. 
Qed. 
End GroupTheory. 

Answer 1

Причина заключается в том, что ваша identity аксиома не зависит от блока e, определенного в разделе, потому что вы связаны с e экзистенциальным квантором в определении identity аксиомы.

Мы можем изменить identity, избавившись от exists e в определении:

Hypothesis identity : forall x : G, (x * e = x) /\ (e * x = x). 

После того, что вы будете в состоянии закончить доказательство.