proposition: Lemma oplus_nf_0 (gamma : T1): nf gamma -> forall alpha beta, nf alpha -> nf beta -> T1.lt alpha gamma -> T1.lt beta gamma -> nf (alpha o+ beta).
proof: Proof. transfinite_induction gamma. - clear gamma ;intros gamma IHgamma H; destruct alpha, beta; auto. intros Hnf_1 Hnf_2 Hlt_1 Hlt_2. nf_decomp Hnf_1; nf_decomp Hnf_2; rewrite oplus_cons_cons; compare destruct alpha1 beta1 as Hcomp. + specialize (IHgamma (phi0 alpha1)). intros; apply nf_intro; [apply nf1| | ]. * eapply IHgamma; trivial. repeat split; auto with T1. -- apply le_lt_trans with (cons alpha1 n alpha2); auto. now apply le_phi0. -- apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n, Hnf_1. -- apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n, Hnf_2. * apply lt_a_phi0_b_oplus; eapply lt_a_phi0_b_intro; eauto. + apply nf_intro; auto. * eapply IHgamma with (phi0 beta1); auto with T1. -- repeat split; auto with T1. apply le_lt_trans with (cons beta1 n0 beta2); auto. apply le_phi0. -- now apply lt_a_phi0_b_phi0, lt_a_phi0_b_intro with n. * apply lt_a_phi0_b_oplus; auto. -- now apply lt_a_phi0_b_phi0R, head_lt. -- now apply lt_a_phi0_b_intro with n. + apply nf_intro; trivial. * eapply IHgamma with (phi0 alpha1); trivial. -- repeat split; auto with T1. apply le_lt_trans with (cons alpha1 n alpha2); auto. apply le_phi0; eauto with T1. -- apply lt_a_phi0_b_phi0. eapply lt_a_phi0_b_intro; eauto. -- now apply head_lt. * apply lt_a_phi0_b_oplus; auto. eapply lt_a_phi0_b_intro; eauto. now constructor 2. Qed.
imports: Coq(Arith ArithRing Lia) hydras(Prelude.More_Arith Prelude.Merge_Sort Epsilon0.T1)