old notes

[kbuzzard]

Found these comments whilst tidying up. Probably no longer relevant:

---

Note:

• The theorem one_eq_succ_zero : 1 = succ 0
  • The theorem ne_iff_implies_false : a ≠ b ↔ (a = b) → false

those are currently undocumented. As is symmetry, rw \l.

[kbuzzard]

The tactics are documented; but I cannot see one_eq_succ_zero or ne_iff_implies_false in the list of theorems.

[kbuzzard]

We never use ne_iff_implies_false; I've removed it.

[kbuzzard]

one_eq_succ_zero is in addition world.