# No subterm matching Hab * a

I am confused. Coq gives the following error:

No subterm matching Hab * a.


What is causing the problem, and how can I solve it?

Definition relation (X Y : Type) := X -> Y -> Prop.
Definition reflexive {X: Type} (R: relation X X) := forall a : X, R a a.
Definition transitive {X: Type} (R: relation X X) := forall a b c : X, (R a b) -> (R b c) -> (R a c).
Definition symmetric {X: Type} (R: relation X X) := forall a b : X, (R a b) -> (R b a).
Definition antisymmetric {X: Type} (R: relation X X) := forall a b : X, (R a b) -> (R b a) -> a = b.
Definition equivalence {X:Type} (R: relation X X) := (reflexive R) /\ (symmetric R) /\ (transitive R).

Open Scope Z_scope.
Require Import ZArith.
Require Import Znumtheory.

Lemma modelus : forall a b c d : Z, (a | b * c) -> Zis_gcd a b d -> (a | c * d).
Proof.
intros a b c d [Hab Hac] [H1 H2].
unfold Z.divide in *.
destruct H1 as [H3 H1].
destruct H2 as [H4 H2].
exists (c * H3 + b * H4).
rewrite <- Hac.
rewrite Z.mul_assoc.
rewrite <- H1.
rewrite <- H2.
reflexivity.

• Isn't the error message self-explanatory? In doing rewrite<- Hac., you're asking to replace all occurrences of Hab * a in the goal by b * c. But there are no occurrences of Hab * a in the goal. May 15 at 21:33
• what is the mathematical argument you want to follow to do this proof in Coq?
– Lolo
May 16 at 0:01
• Please understand that the edit history is always available for everyone to see. You may leave a question as is even if it is resolved for you, in case it receives future answers and/or helps other visitors. If you have specific reasons that you want to remove some information from the question, please let me know.
– Trebor
May 17 at 17:04
• This is just a problem with the left-associativity of the operator * in Coq. The term c * x * a is read (c * x) * a and not c * (x * a). You may use the associativity of multiplication before your rewrite. P.S. Why calling Haban integer ? May 18 at 14:20