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