proposition: Lemma plus_mono_l_weak: forall o, nf o -> forall alpha, nf alpha -> alpha < o -> forall beta, nf beta -> beta < o -> forall gamma , nf gamma -> alpha < beta -> alpha + gamma <= beta + gamma.
proof: Proof. intros o Ho;pattern o. apply transfinite_induction. 2:auto with T2. clear o Ho. intros o NF0 Hreco. intro x;case x. simpl. intros;apply le_plus_l;auto with T2. intros alpha beta n gamma NF. intro. intro y;case y. inversion 4. intros alpha' beta' n' gamma' NF'. intros H1 z. case z. do 2 rewrite (plus_alpha_0). right;auto with T2. intros alpha'' beta'' n'' gamma'' NF''. intros H0. simpl (cons alpha beta n gamma + cons alpha'' beta'' n'' gamma''). caseEq ( compare [alpha, beta] [alpha'', beta'']). intro H'; generalize (compare_eq_rw H'); intro H''. injection H'';intros. subst alpha'';subst beta''. simpl (cons alpha' beta' n' gamma' + cons alpha beta n'' gamma''). caseEq ( compare [alpha', beta'] [alpha, beta]). intro H6; generalize (compare_eq_rw H6); intro H7. injection H7;intros;subst alpha';subst beta'. case (le_inv_nc (or_intror _ H0)). right;constructor 6. auto with T2 arith. intros (H8,H9);subst n'. left;auto with T2. intro H6; generalize (compare_lt_rw H6); intro H7. case (lt_irr (alpha := cons alpha beta n gamma)). apply transitivity with (cons alpha' beta' n' gamma');auto with T2. apply psi_relevance;auto with T2. intros;right;apply psi_relevance. apply compare_gt_rw;auto with T2. intro H'; generalize (compare_lt_rw H'); intro H''. simpl (cons alpha' beta' n' gamma' + cons alpha'' beta'' n'' gamma''). caseEq (compare [alpha', beta'] [alpha'', beta'']). intro H6; generalize (compare_eq_rw H6); intro H7. injection H7;intros;subst alpha';subst beta'. right;constructor 6;auto with T2 arith. intro H6; generalize (compare_lt_rw H6); intro H7. left;auto with T2. intro H6; generalize (compare_gt_rw H6); intro H7. right;apply psi_relevance;auto with T2. intro H'; generalize (compare_gt_rw H'); intro H''. assert ([alpha'',beta''] < [alpha',beta']). apply lt_le_trans with [alpha,beta];auto with T2. generalize (le_psi_term_le (or_intror _ H0)). simpl;auto with T2. simpl ( cons alpha' beta' n' gamma' + cons alpha'' beta'' n'' gamma''). caseEq ( compare [alpha', beta'] [alpha'', beta'']). intro H6; generalize (compare_eq_rw H6); intro H7. rewrite H7 in H2. case (lt_irr H2). intro H6; generalize (compare_lt_rw H6); intro H7. case (lt_irr (alpha := [alpha'', beta''])). apply transitivity with [alpha', beta'];auto with T2. intro H6; generalize (compare_gt_rw H6); intro H7. tricho [alpha, beta] [alpha', beta'] H8. right;apply psi_relevance;auto with T2. injection H8;intros;subst alpha';subst beta'. case (le_inv_nc (or_intror _ H0)). right;constructor 6;auto with T2. intros (e,H9);subst n'. case H9. intro;subst gamma'. left;auto with T2. intro H10. assert (nf gamma). inversion NF;auto with T2. assert (nf gamma'). inversion NF';auto with T2. assert (gamma < cons alpha beta n gamma'). apply transitivity with gamma'. auto with T2. apply lt_tail;auto with T2. generalize (Hreco _ NF' H1 gamma H3 H5 gamma' H4 (lt_tail NF') (cons alpha'' beta'' n'' gamma'') NF'' H10). destruct 1;auto with T2. rewrite H11;auto with T2. case (lt_irr (alpha := cons alpha beta n gamma)). apply transitivity with (cons alpha' beta' n' gamma');auto with T2. apply psi_relevance;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