proposition: Lemma plus_mono_r : forall alpha , nf alpha -> forall beta gamma, nf beta -> nf gamma -> beta < gamma -> alpha + beta < alpha + gamma.
proof: Proof. induction alpha. simpl. auto with T2. simpl. destruct beta;destruct gamma;simpl. inversion 3. intros; caseEq (compare (cons alpha1 alpha2 0 zero) (cons gamma1 gamma2 0 zero)). constructor 6. omega. intros;apply psi_relevance. apply compare_lt_rw;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. caseEq (compare (cons alpha1 alpha2 0 zero) (cons beta1 beta2 0 zero)); caseEq ( compare (cons alpha1 alpha2 0 zero) (cons gamma1 gamma2 0 zero)). intros. generalize (compare_eq_rw H1). generalize (compare_eq_rw 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;omega. constructor 7;auto with T2. intros. generalize (compare_lt_rw H0). generalize (compare_eq_rw H1). intros;apply psi_relevance. auto with T2. intros. generalize (compare_gt_rw H0). generalize (compare_eq_rw H1). injection 1;intros. subst beta1;subst beta2. case (lt_irr (alpha := (cons alpha1 alpha2 n0 beta3))). eapply transitivity. eexact H4. apply psi_relevance;auto with T2. intros. generalize (compare_lt_rw H1). generalize (compare_eq_rw H0). injection 1;intros. subst gamma1;subst gamma2. case (lt_irr (alpha :=cons beta1 beta2 n0 beta3)). eapply transitivity. eexact H4. apply psi_relevance;auto with T2. auto with T2. intros. case (lt_irr (alpha := (cons beta1 beta2 n0 beta3))). eapply transitivity. eexact H4. apply psi_relevance. apply transitivity with (cons alpha1 alpha2 0 zero);auto with T2. intros. generalize (compare_eq_rw H0). injection 1;intros;subst gamma1;subst gamma2. constructor 6;omega. intros. apply psi_relevance. auto with T2. intros. constructor 7. apply IHalpha3. inversion H;auto with T2. auto with T2. auto with T2. auto with T2. Qed.
imports: EPSILON0 Arith List Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP not_decreasing EPSILON0 More_nat Gamma0_prelude Gamma0_length term rpo