proposition: Lemma le_phi0_phi0 : forall a b, a <= b -> phi0 a <= phi0 b.
proof: Proof. destruct 1. subst b;left;auto. right;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