Rewrite and equatorial reasoning in agde

Question

With rewriting, I have a concise syntax (for example, no congruence property is called), and I can prove:

-- * is associative *-assoc : ∀ abc → (a * b) * c ≡ a * (b * c) *-assoc zero bc = refl *-assoc (succ a) bc rewrite *+-dist b (a * b) c | *-assoc abc = refl 

however my little brain can better analyze this evidence

 --written in equational style *-assoc' : ∀ abc → (a * b) * c ≡ a * (b * c) *-assoc' zero bc = refl *-assoc' (succ a) bc = (succ a * b) * c ≡⟨ refl ⟩ (b + a * b) * c ≡⟨ *+-dist b (a * b) c ⟩ b * c + (a * b) * c ≡⟨ cong (λ x -> b * c + x) (*-assoc abc) ⟩ b * c + a * (b * c) ≡⟨ refl ⟩ (succ a) * (b * c) ∎ 

but I have to indicate which subterm "transform", causing congruence.

Is there a way to combine rewriting and equational notation to get rid of the mention of congruence?

Thank you in advance