proposition: Lemma inject_mono_0 : forall alpha, T1.nf alpha -> forall beta gamma, T1.lt beta gamma -> T1.lt gamma alpha -> T1.nf beta -> T1.nf gamma -> (inject beta < inject gamma)%sch.
proof: Proof. Proof with eauto with T1. intros alpha; T1.transfinite_induction alpha. intros x Indx Nx; induction beta; destruct gamma. { intros H H0; T1.T1_inversion H. } { intros H H0 H1 H2; simpl; apply lt_le_trans with (AP._phi0 (inject gamma1))%sch. - apply phi0_positive;auto with schutte. - eapply le_trans. 2:eapply le_plus_l; auto with schutte. apply le_a_mult_Sn_a; auto with schutte. } intros H H0 H1 H2; T1.T1_inversion H. intros H H0 H1 H2; simpl; destruct (T1.lt_inv H). - apply head_lt. + eapply IHbeta1 ... * apply T1.lt_trans with (T1.cons gamma1 n0 gamma2) ... + apply lt_trans with (inject (T1.phi0 beta1)). * eapply IHbeta2 ... apply T1.lt_a_phi0_b_phi0. apply T1.lt_a_phi0_b_intro with n; auto. apply Comparable.le_lt_trans with (T1.cons beta1 n beta2); auto with T1. apply T1.le_phi0 ; eauto with T1. eapply T1.lt_trans ... * simpl; rewrite alpha_plus_zero. apply phi0_mono, IHbeta1; auto. apply T1.lt_trans with (T1.cons gamma1 n0 gamma2) ... eauto with T1. eauto with T1. - decompose [or and] H3. subst; apply coeff_lt. + replace (AP._phi0 (inject gamma1)) with (inject (T1.phi0 gamma1)). * apply IHbeta2. apply T1.lt_a_phi0_b_phi0. eapply T1.lt_a_phi0_b_intro; eauto. apply Comparable.le_lt_trans with (T1.cons gamma1 n0 gamma2); auto. destruct n0. apply T1.le_tail ... apply Comparable.lt_incl_le. apply T1.coeff_lt; auto with arith. eauto with T1. eapply T1.nf_phi0; eauto with T1. * cbn; rewrite alpha_plus_zero ... + auto. + subst; apply plus_mono_r. apply IHbeta2; eauto with schutte T1. eapply T1.lt_trans. 2: eapply H0. auto with T1. apply T1.tail_lt_cons; auto. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)