proposition: Lemma plus_nf0 : forall a, nf a -> forall b c, b < phi0 a -> c < phi0 a -> nf b -> nf c -> nf (b + c).
proof: Proof. intros a Ha ; pattern a. apply transfinite_induction. 2:assumption. intros x Cx Hx. destruct b; destruct c. simpl;constructor. simpl;auto. intros;rewrite plus_a_zero; auto. intros. case (trichotomy_inf b1 c1). destruct 1. rewrite plus_cons_cons_rw1. auto. auto. subst c1. rewrite plus_cons_cons_rw2. eapply nf_coeff_irrelevance;eauto. auto. auto. intro; rewrite plus_cons_cons_rw3;auto. apply nf_intro. nf_inv. eapply Hx with b1. nf_inv. inversion_clear H; auto. inversion H3. inversion H3. inversion H1. compute;auto with T1. unfold phi0. constructor 2;auto. unfold phi0. constructor 2;auto. nf_inv. auto. apply nf2_phi0R. apply ap_plus. unfold phi0;constructor. nf_inv. auto. apply nf2_phi0. eapply nf2_intro. eauto. 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