proposition: Lemma phi_spec2 a x: T2nf a -> T2nf x -> (forall c, T2nf c -> c < a -> phi c x = x) -> a <= T2_pr1 x.
proof: Proof. move => na nx ha. move: (limit_pr1 a). case az: (a==zero); first by rewrite (eqP az) T2le0n. have hb: phi zero x = x by apply: ha => //; rewrite T2lt0n az. have eq1: x = [T2_pr1 x, T2_pr2 x] by move: (phi_ap zero x); rewrite hb. case la: (T2limit a) => h. case (T2ltP (T2_pr1 x) a) => // sa. move: (limit_pr la sa) => /ha hc. have aux: T2nf (T2succ (T2_pr1 x)). by apply: nf_succ; move: nx; case x => // a' b' n' c' /= /and4P []. by move: (phi_le1 (T2succ (T2_pr1 x)) x); rewrite hc // T2leNgt succ_lt. move: (succ_pred na h) => nsa. move: (succ_lt (T2pred a)); rewrite - nsa => /ha => eq. have aux: T2nf (T2pred a). by apply: nf_pred; move: na; case x => // a' b' n' c' /= /and4P []. move: (eq aux); rewrite eq1 /=; case hc: (T2pred a < T2_pr1 x). by rewrite nsa - lt_succ_le_4 //; move: nx; rewrite {1} eq1 /= =>/andP []. case => _ hd. by move: (T2lt_ne (T2lt_psi_b (T2_pr1 x) (T2_pr2 x))); rewrite hd eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)