vstd::arithmetic::mul

Function lemma_mul_strictly_positive

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

Proof that multiplication distributes over addition and subtraction, whether the addition or subtraction happens in the first or the second argument to the multiplication. Proof that if x and y are both positive, then their product is also positive.