Function vstd::arithmetic::div_mod::lemma_div_basics_2
source · pub broadcast proof fn lemma_div_basics_2(x: int)Expand description
ensures
#[trigger] (x / 1) == x,pub broadcast proof fn lemma_div_basics_2(x: int)#[trigger] (x / 1) == x,