Coq: Unzureichende Begründung Fehler

Question

Ich bin neu in Coq und bekomme einen Insufficient Justification Fehler für die Hypothese H3. Ich habe versucht, es mehrmals umzuschreiben, aber der Fehler bleibt bestehen. Könnte jemand bitte erklären warum? Vielen Dank.

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

Der Grund dafür ist, dass Ihr identity Axiom ist unabhängig von der Einheit e im Abschnitt definiert, da Sie e mit dem Existenzquantor in der Definition des identity Axiom gebunden haben.

Wir identity ändern können, erhalten von exists e in der Definition los:

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

Danach Sie in der Lage sein, Ihren Beweis zu beenden.