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