proposition: Lemma plus_nf0 : forall a, nf a -> forall b c, lt b (phi0 a) -> lt c (phi0 a) -> nf b -> nf c -> nf (b + c).
proof: Proof. intros a; pattern a; transfinite_induction_lt a. intros x Cx Hx. destruct b; destruct c. - simpl;constructor. - simpl;auto with T1. - intros;rewrite plus_zero_r; auto with T1. - intros; case (lt_eq_lt_dec b1 c1). + destruct 1. * rewrite plus_cons_cons_rw1; auto with T1. * subst c1; rewrite plus_cons_cons_rw2; auto with T1. + intro; rewrite plus_cons_cons_rw3;auto with T1. apply nf_intro. * eapply nf_inv1;eauto with T1. * nf_decomp H1; nf_decomp H2. eapply Cx with b1; trivial. apply lt_a_phi0_b_inv in H;auto with T1. apply lt_a_phi0_b_phi0. eapply lt_a_phi0_b_intro with n; trivial. apply lt_a_phi0_b_phi0. eapply lt_a_phi0_b_intro with n0; trivial. apply cons_nf; auto. * nf_decomp H1; nf_decomp H2. apply lt_a_phi0_b_phi0R; apply ap_plus; trivial. constructor. apply lt_a_phi0_b_phi0. eapply lt_a_phi0_b_intro; trivial. auto with T1. Unshelve. exact 0. Defined.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)