Function vstd::arithmetic::mul::lemma_mul_equality_converse

source · 
pub broadcast proof fn lemma_mul_equality_converse(m: int, x: int, y: int)
Expand description
requires
m != 0,
#[trigger] (m * x) == #[trigger] (m * y),
ensures
x == y,

Proof that if x and y have equal results when multiplied by nonzero m, then they’re equal