vstd::arithmetic::div_mod

Function lemma_div_basics_2

Source
pub broadcast proof fn lemma_div_basics_2(x: int)
Expand description
ensures
#[trigger] (x / 1) == x,

Proof for basic property that x divided by 1 is x.