proposition: Lemma le_plus_l : forall alpha beta, nf alpha -> nf beta -> alpha t2<= beta + alpha.
proof: Proof. induction alpha. - intros;apply le_zero_alpha. - destruct beta. + cbn;auto with T2. + cbn; intros; case_eq(compare (gcons beta1 beta2 0 zero) (gcons alpha1 alpha2 0 zero)). * intros; generalize (compare_Eq H1). injection 1. intros;subst beta1;subst beta2. right;constructor 6; lia. * left;auto with T2. * intros;right;apply psi_lt_head. apply compare_Gt; 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)