function

Stream: new members

[vxctyxeha]

how to solve this problem
h_step2 : y * 2 = f y * 2
h2ne0 : 2 ≠ 0
⊢ f y = y
image.png

[Niels Voss]

Can you provide some more context (preferably a #mwe)? Right now it basically seems like you want to divide h_step2 by 2 (perhaps by using apply or apply_fun), but without knowing what the types of y and 2 are it is hard to help. (For example, this statement is false in general if you are working over ZMod 6)