Function vstd::arithmetic::mul::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