Added TODO: Direct proof using of pred-N using N-least-pre-fixed.
Added induction instances examples.