add lt to peano.hs + add comments on proof by simplification / forall