Beginning with induction
First inductions
More induction examples
Finished mult_comm
Simpl, descruct, induction exercises
Binary_commute proved
Induction chapter done