Let c and t be given.

Assume HcR: c ∈ R.

Assume HtR: t ∈ R.

rewrite the current goal using (mul_const_fun_apply c t HcR HtR) (from left to right).

An exact proof term for the current goal is (real_mul_SNo t HtR c HcR).

∎