proposition: Lemma plus_mono_l_weak: forall o, nf o -> forall alpha, nf alpha -> alpha t2< o -> forall beta, nf beta -> beta t2< o -> forall gamma , nf gamma -> alpha t2< beta -> alpha + gamma t2<= beta + gamma.
proof: Proof. intros o Ho;pattern o. apply transfinite_induction; [| auto with T2]. clear o Ho; intros o NF0 Hreco. intro x;case x. - cbn; 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' H1 z; case z. do 2 rewrite (plus_alpha_0). right;auto with T2. intros alpha'' beta'' n'' gamma'' NF'' H0. simpl (gcons alpha beta n gamma + gcons alpha'' beta'' n'' gamma''). case_eq ( compare [alpha, beta] [alpha'', beta'']). intro H'; generalize (compare_Eq H'); intro H''. injection H'';intros. subst alpha'';subst beta''. simpl (gcons alpha' beta' n' gamma' + gcons alpha beta n'' gamma''). case_eq ( compare [alpha', beta'] [alpha, beta]). intro H6; generalize (compare_Eq 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 H6); intro H7. case (lt_irr (alpha := gcons alpha beta n gamma)). apply lt_trans with (gcons alpha' beta' n' gamma');auto with T2. apply psi_lt_head;auto with T2. * intros;right;apply psi_lt_head. apply compare_Gt;auto with T2. * intro H'; generalize (compare_Lt H'); intro H''. simpl (gcons alpha' beta' n' gamma' + gcons alpha'' beta'' n'' gamma''). case_eq (compare [alpha', beta'] [alpha'', beta'']). -- intro H6; generalize (compare_Eq H6); intro H7. injection H7;intros;subst alpha';subst beta'. right;constructor 6;auto with T2 arith. -- intro H6; generalize (compare_Lt H6); intro H7. left;auto with T2. -- intro H6; generalize (compare_Gt H6); intro H7. right;apply psi_lt_head;auto with T2. * intro H'; generalize (compare_Gt H'); intro H''. assert ([alpha'',beta''] t2< [alpha',beta']). { apply lt_le_trans with [alpha,beta];auto with T2. generalize (le_psi_term_le (or_intror _ H0)). cbn;auto with T2. } simpl ( gcons alpha' beta' n' gamma' + gcons alpha'' beta'' n'' gamma''). case_eq ( compare [alpha', beta'] [alpha'', beta'']). -- intro H6; generalize (compare_Eq H6); intro H7. rewrite H7 in H2. case (lt_irr H2). -- intro H6; generalize (compare_Lt H6); intro H7. case (lt_irr (alpha := [alpha'', beta''])). apply lt_trans with [alpha', beta'];auto with T2. -- intro H6; generalize (compare_Gt H6); intro H7. tricho [alpha, beta] [alpha', beta'] H8. ++ right;apply psi_lt_head;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 t2< gcons alpha beta n gamma'). apply lt_trans with gamma'. auto with T2. apply lt_tail;auto with T2. generalize (Hreco _ NF' H1 gamma H3 H5 gamma' H4 (lt_tail NF') (gcons alpha'' beta'' n'' gamma'') NF'' H10). destruct 1;auto with T2. rewrite H11;auto with T2. ++ case (lt_irr (alpha := gcons alpha beta n gamma)). apply lt_trans with (gcons alpha' beta' n' gamma');auto with T2. apply psi_lt_head;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)