Tactic for explicit type coercion

Stream: new members

[Bo Qin]

How do I the type coercion from

F (k + 1) + F k := by rw[F]

to

_ > 0.4 * 1.6 ^ (k + 1) + 0.4 * 1.6 ^ k := by rel[IH1a, IH2a]

where do I put the ( :\Q)?
math3.png

[Bo Qin]

of course this fails at F because of different return type?
math3a.png

[Aaron Liu]

try putting it everywhere

[Bo Qin]

I can't seem to do the coersion of a function, but it works for primitive types

[Bo Qin]

this fails the rw tactics
math3b.png

[Aaron Liu]

you have to rewrite with a casting theorem