Propositions on rational integers

Stream: Is there code for X?

[Ryan Gold]

Is there some code that can turn a proposition like ↑ (a * b) = ↑ (c) into a * b = c, where (a b c : ℤ ) provided with evidence that the denominators of each term are 1?

My gut says it's related to monads somehow, but I haven't quite worked through that library yet.

[Gabriel Ebner]

What you've written looks like its true by norm_cast without any assumptions. But maybe I've misinterpreted the coercion.

[Ryan Gold]

No, that seems right! It looks like I should get a bit more familiar with that tactic. Thanks!