proposition: Theorem th_14_6 : forall alpha1 beta1 alpha2 beta2, nf alpha1 -> nf beta1 -> nf alpha2 -> nf beta2 -> phi alpha1 beta1 < phi alpha2 beta2 -> {alpha1 < alpha2 /\ beta1 < phi alpha2 beta2} + {alpha1 = alpha2 /\ beta1 < beta2} + {alpha2 < alpha1 /\ phi alpha1 beta1 < beta2}.
proof: Proof. intros alpha1 beta1 alpha2 beta2 nfa1 nfb1 nfa2 nfb2 E. tricho alpha1 alpha2 H0. generalize (phi_to_psi alpha2 beta2). intros (gamma1, (gamma2, E')). assert (alpha2 <= gamma1). eapply phi_le. 2:eexact E'. auto. left. left;split;auto. apply le_lt_trans with (phi alpha1 beta1);auto. apply le_b_phi_ab;auto. subst alpha2. left;right. split;auto. tricho beta1 beta2 H;auto. subst beta2;case (lt_irr E). case (lt_not_gt E). apply phi_mono_r;auto. right. split;auto. generalize (phi_to_psi alpha1 beta1). intros (gamma1, (gamma2, E')). assert (alpha1 <= gamma1). apply phi_le with beta1 gamma2. auto. auto. assert (alpha2 < gamma1). apply lt_le_trans with alpha1;auto. assert (phi alpha2 (phi alpha1 beta1) = phi alpha1 beta1). repeat rewrite E'. simpl. rewrite (compare_rw_lt H1). auto. assert (phi alpha2 (phi alpha1 beta1) < phi alpha2 beta2). eapply le_lt_trans. eleft;eexact H2. auto. apply phi_mono_RR with alpha2;auto. apply phi_nf;auto. 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