Function vstd::arithmetic::div_mod::lemma_div_is_strictly_smaller

source · 
pub broadcast proof fn lemma_div_is_strictly_smaller(x: int, d: int)
Expand description
requires
0 < x,
1 < d,
ensures
#[trigger] (x / d) < x,

Proof that a number gets strictly smaller when divided by a number greater than one. Specifically, x / d < x.