vstd::arithmetic::div_mod

Function lemma_div_by_self

Source 
pub proof fn lemma_div_by_self(d: int)
Expand description
requires
d != 0,
ensures
d / d == 1,

Proof that the quotient of an integer divided by itself is 1, specifically that d / d == 1.