proposition: Lemma phi_mono_r : forall a b c, nf a -> nf b -> nf c -> b < c -> phi a b < phi a c.
proof: Proof. intros a b c Ha Hb Hc H. case (phi_cases' a Hb). destruct 1. case s; intros b1 (b2,(H1,(H2,H3))). rewrite H3. apply lt_le_trans with c;auto with T2. apply le_b_phi_ab;auto with T2. case (phi_cases' a Hc). destruct 1. case s; intros c1 (c2,(H'1,(H'2,H'3))). rewrite e. rewrite H'3. rewrite H'1. constructor 2;auto with T2. rewrite H'1 in H. auto with T2. rewrite e;rewrite e0;auto with T2. intros (c1,(c2,(n, (H1,(H2,H3))))). subst c. assert ((cons c1 c2 0 (finite (S n))) = (succ (cons c1 c2 0 (finite n)))). simpl;auto with T2. caseEq c1. intro; subst c1; lt_clean. case n;auto with T2. assert (nf (cons c1 c2 0 (finite n))). case n. inversion Hc;auto with T2. inversion Hc;auto with T2. intro; simpl; constructor. constructor 2. apply le_lt_trans with a;auto with T2. auto with T2. inversion Hc;auto with T2. inversion Hc;auto with T2. repeat constructor. rewrite H0 in H. case (succ_lt_le Hb H1 H). intro;subst b. case (lt_irr (alpha:=[a, (cons c1 c2 0 (finite n))])). pattern [ a, (cons c1 c2 0 (finite n))] at 1;rewrite <- e. apply phi_of_psi_plus_finite. auto with T2. rewrite H3. rewrite e. auto with T2. intros (b1,(b2,(n,(H1,(H2,H3))))). case (phi_cases' a Hc). destruct 1. case s;intros c1 (c2,(H'1,(H'2,H'3))). rewrite H3;rewrite H'3;rewrite H'1. subst b; subst c;case n;simpl;auto with T2. constructor 2. auto with T2. apply le_lt_trans with (cons b1 b2 0 (finite (S n))). simpl;auto with arith T2. auto with T2. constructor 2. auto with T2. inversion H; auto with T2. lt_clean. rewrite H3; rewrite e. apply transitivity with [a, (cons b1 b2 0 (finite (S n)))]. case n;simpl;auto with T2. subst b;auto with T2. intros (c1,(c2,(p,(H'1,(H'2,H'3))))). rewrite H'3;rewrite H3. subst c;subst b. generalize H;inversion 1;auto with T2. constructor 3. constructor 7. apply lt_compatR. inversion H4;lt_clean; 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