proposition: Lemma phi0_ltR : forall a b, phi0 a < phi0 b -> a < b.
proof: Proof. unfold phi0;intros c c' H. case (lt_inv H). trivial. intros [(_,i)|(_,(_,i))]; inversion i. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List