proposition: Lemma phi0_log : forall a, a < phi0 (succ (log a)).
proof: Proof. destruct a. simpl. compute. constructor. simpl. unfold phi0. constructor 2. apply lt_succ. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List