proposition: Lemma plus_mono_r : forall alpha , nf alpha -> forall beta gamma, nf beta -> nf gamma -> beta t2< gamma -> alpha + beta t2< alpha + gamma.
proof: Proof. induction alpha. - cbn; auto with T2. - cbn; destruct beta;destruct gamma;cbn. + inversion 3. + intros; case_eq (compare (gcons alpha1 alpha2 0 zero) (gcons gamma1 gamma2 0 zero)). * constructor 6; lia. * intros;apply psi_lt_head. apply compare_Lt;auto with T2. * constructor 7. pattern alpha3 at 1; rewrite <- plus_alpha_0. apply IHalpha3. inversion H;auto with T2. auto with T2. auto with T2. auto with T2. + inversion 3. + case_eq (compare (gcons alpha1 alpha2 0 zero) (gcons beta1 beta2 0 zero)); case_eq (compare (gcons alpha1 alpha2 0 zero) (gcons gamma1 gamma2 0 zero)). intros H0 H1 H2 H3 H4; generalize (compare_Eq H1); generalize (compare_Eq H0). * injection 1. injection 3. subst gamma1;subst gamma2;intros; subst beta2;subst beta1. inversion_clear H4. case (lt_irr H6). case (lt_irr H6). case (lt_irr H6). case (lt_irr H6). constructor 6;lia. constructor 7;auto with T2. * intros H0 H1 H2 H3 H4; generalize (compare_Lt H0); generalize (compare_Eq H1). intros;apply psi_lt_head. auto with T2. * intros. generalize (compare_Gt H0). generalize (compare_Eq H1). injection 1;intros. subst beta1;subst beta2. case (lt_irr (alpha := (gcons alpha1 alpha2 n0 beta3))). eapply lt_trans. eexact H4. apply psi_lt_head;auto with T2. * intros. generalize (compare_Lt H1). generalize (compare_Eq H0). injection 1;intros. subst gamma1;subst gamma2. case (lt_irr (alpha :=gcons beta1 beta2 n0 beta3)). eapply lt_trans. eexact H4. apply psi_lt_head;auto with T2. * auto with T2. * intros; case (lt_irr (alpha := (gcons beta1 beta2 n0 beta3))). eapply lt_trans. eexact H4. apply psi_lt_head. apply lt_trans with (gcons alpha1 alpha2 0 zero);auto with T2. * intros; generalize (compare_Eq H0). injection 1;intros;subst gamma1;subst gamma2. constructor 6;lia. * intros; apply psi_lt_head. auto with T2. * intros; constructor 7. apply IHalpha3. inversion H;auto with T2. auto with T2. auto with T2. auto with T2. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)