proposition: Lemma lt_phi0_phi0 : forall a b, a < b -> phi0 a < phi0 b.
proof: Proof. unfold phi0. constructor 2. auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List