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.