proposition: Lemma psi_principal : forall a b c d, nf c -> c < [a, b] -> d < [a, b] -> c + d < [a, b].
proof: Proof. induction c;destruct d;simpl;auto with T2. case (compare [c1,c2][d1,d2]). intros;apply psi_relevance. inversion_clear H0. constructor 2;auto with T2. constructor 3;auto with T2. constructor 4;auto with T2. constructor 5;auto with T2. inversion H2. inversion H2. auto with T2. intros. generalize (IHc3 (cons d1 d2 n0 d3)). intros. assert (c3 < [a,b]). eapply transitivity. 2:eexact H0. apply lt_tail. auto with T2. inversion_clear H0. constructor 2;auto with T2. constructor 3;auto with T2. constructor 4;auto with T2. constructor 5;auto with T2. inversion H4. constructor 7;auto with T2. inversion H4. 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