There is a very useful website where you can prove these basic concepts one by one, they made a little game out of it, in order to show the underlying software,

There is a very useful website where you can prove these basic concepts one by one, they made a little game out of it, in order to show the underlying software, which is leanprover: https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g...