nat.bend checks

Nat.add — the first two lemmas: a + 0 == a, and (a + b) + c == a + (b + c).

Base ships a rich term library and no reasoning library; these are the two facts every proof over Nat.add ends up writing by hand. A lemma is a def whose return type is an equation; import this package and call one by name.

add_zero: a + 0 == a (Nat.add recurses on its first argument, so Nat.add(a, 0n) is stuck when a is a variable) add_assoc: (a + b) + c == a + (b + c)