exercises done in Basics.v (+ comments) up to "Proof by Simplification"