proposition: Lemma le_plus_r : forall alpha beta, nf alpha -> nf beta -> alpha <= alpha + beta.
proof: Proof. induction alpha. intros;apply le_zero_alpha. destruct beta. intros; rewrite plus_alpha_0;auto with T2. simpl. intros; caseEq( compare (cons alpha1 alpha2 0 zero) (cons beta1 beta2 0 zero)). right;constructor 6. omega. intros;right;apply psi_relevance. apply compare_lt_rw. auto with T2. intro; apply le_cons_tail. apply IHalpha3. inversion H;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