proposition: Lemma phi0_lt : forall a b, a < b -> phi0 a < phi0 b.
proof: Proof. unfold phi0;intros c c' H. constructor 2;trivial. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List