Function vstd::arithmetic::div_mod::lemma_div_basics
source · pub proof fn lemma_div_basics(x: int)
Expand description
ensures
x != 0 as int ==> 0 as int / x == 0,
x / 1 == x,
x != 0 ==> x / x == 1,
Proof establishing basic properties of division using x
: 0
divided by x
is 0; x
divided by 1 is itself; and x
divided
by itself is 1.