Function vstd::arithmetic::div_mod::lemma_div_non_zero
source · pub proof fn lemma_div_non_zero(x: int, d: int)
Expand description
requires
x >= d > 0,
ensures#[trigger] (x / d) > 0,
Proof that division of a positive integer by a positive integer
less than or equal to it is nonzero. Specifically, given that x >= d
, we can conclude that x / d > 0
.