Function vstd::arithmetic::div_mod::lemma_div_is_div_recursive

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

Proof that, for the case of x / d, division using / is equivalent to a recursive definition of division