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