Proofs with coercion

Stream: new members

[Sarah Linh]

I'm trying out proofs in Lean and encountered this : (max (↑rs1_val.toNat * rs2_val.toInt) 0)) = (max (rs1_val.toInt * rs2_val.toInt) 0)) where ↑x represents a coercion, which converts x of type Nat to type Intand rs1 and rs2 are of BitVec 64. Can someone help me with an approach to proof this or give me some pointers? I'm unsure how to handle the coercion, thx

[Ruben Van de Velde]

I suggest you share a #mwe (that's a link, please read it). Then we can look at the exact state that you're having trouble with, rather than second-guessing what your issue might be

[Sarah Linh]

thank you, I managed to solve it in the meantime.