feat(04_Quantifiers_and_Equality): remove exercise that is too difficult
feat(04_Quantifiers_and_Equality): remove exercise that is too difficult

I think this is too difficult at this stage. Indeed if I am not
mistaken, a correct statement of the analogue identity would be a
conditional one, like:

y <= x -> (x - y) * (x - y) = x * x - x * y - x * y - y * y

because for x > y, the equality does not hold on the nat semi-ring:
e.g. for y = x + 1, left hand side is 0 but right hand side is 2.

leanprover/tutorial,soonhokong/lean-tutorial,Hodapp87/cs6460_project,cjmazey/fork_leanprover_tutorial,soonhokong/lean-tutorial,soonhokong/lean-tutorial,leanprover/tutorial,avigad/tutorial,cjmazey/fork_leanprover_tutorial,cjmazey/fork_leanprover_tutorial,fpvandoorn/tutorial,fpvandoorn/tutorial,avigad/tutorial,Hodapp87/cs6460_project,avigad/tutorial,Hodapp87/cs6460_project,leanprover/tutorial,fpvandoorn/tutorial