proposition: Lemma phi_inj_r : forall a b c, nf a -> nf b -> nf c -> phi a b = phi a c -> b= c.
proof: Proof. intros a b c Na Nb Nc E. tricho b c H. absurd (phi a b < phi a c). rewrite E. apply lt_irr. apply phi_mono_r;auto. auto. absurd (phi a c < phi a b). rewrite E. apply lt_irr. apply phi_mono_r;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