proposition: Lemma lt_a_phi0_a : forall a, a < phi0 a.
proof: Proof. induction a;simpl. compute; constructor. unfold phi0. constructor 2. assert (le (cons a1 0 zero) (cons a1 n a2)). case n. case a2. left. trivial. right;constructor 4;constructor. right;constructor 3. auto with arith. case H. injection 1. intros; subst a2;subst n;auto. intro; eapply lt_trans; eauto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List