Function vstd::arithmetic::div_mod::lemma_small_div_converse

pub broadcast proof fn lemma_small_div_converse(x: int, d: int)

Expand description

ensures

0 <= x && 0 < d && #[trigger] (x / d) == 0 ==> x < d,

Proof that if a dividend is a whole number, the divisor is a natural number, and their quotient is 0, then the dividend is smaller than the divisor