Let A, f, c and x be given.

Assume HxA: x ∈ A.

Assume HcR: c ∈ R.

Assume HfxR: apply_fun f x ∈ R.

rewrite the current goal using (compose_fun_apply A f (div_const_fun c) x HxA) (from left to right).

rewrite the current goal using (div_const_fun_apply c (apply_fun f x) HcR HfxR) (from left to right).

Use reflexivity.

∎