pub broadcast proof fn lemma_div_basics_3(x: int)
x != 0 ==> #[trigger] (x / x) == 1,
Proof for basic property that x divided by x is 1.
x