Skip to content

Instantly share code, notes, and snippets.

@fionn

fionn/two_plus_two_eq_four.lean

Last active October 25, 2025 18:12
Show Gist options
  • Save fionn/e41cd93a141a1ff69b47a64477e1ca1e to your computer and use it in GitHub Desktop.
Save fionn/e41cd93a141a1ff69b47a64477e1ca1e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
two_plus_two_eq_four.lean
rw [four_eq_succ_three]
rw [three_eq_succ_two]
repeat rw [two_eq_succ_one]
repeat rw [one_eq_succ_zero]
repeat rw [add_succ]
repeat rw [add_succ]
rw [add_zero]
rfl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment