Proof of 'forall n, n^n >= factoral n' to get used to proving theorems about fixpoint-defined functions