proposition: Lemma phi_mono_r : forall a b c, nf a -> nf b -> nf c -> b t2< c -> phi a b t2< 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 ((gcons c1 c2 0 (fin (S n))) = (succ (gcons c1 c2 0 (fin n)))). { simpl;auto with T2. case_eq c1. intro; subst c1; lt_clean. case n;auto with T2. } assert (nf (gcons c1 c2 0 (fin n))). { case n. inversion Hc;auto with T2. inversion Hc;auto with T2. intro; cbn; 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, (gcons c1 c2 0 (fin n))])). pattern [ a, (gcons c1 c2 0 (fin n))] at 1;rewrite <- e. apply phi_of_psi_plus_fin. auto with T2. -- rewrite H3, 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 (gcons b1 b2 0 (fin (S n))). ++ cbn;auto with arith T2. ++ auto with T2. -- constructor 2; auto with T2. inversion H; auto with T2. lt_clean. * rewrite H3; rewrite e. apply lt_trans with [a, (gcons b1 b2 0 (fin (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: 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)