Function vstd::arithmetic::mul::lemma_mul_nonzero

source · 
pub broadcast proof fn lemma_mul_nonzero(x: int, y: int)
Expand description
ensures
#[trigger] (x * y) != 0 <==> x != 0 && y != 0,

Proof that x * y is nonzero if and only if both x and y are nonzero