pub proof fn lemma_div_by_self(d: int)
d != 0,
d / d == 1,
Proof that the quotient of an integer divided by itself is 1, specifically that d / d == 1.
d / d == 1