proposition: Lemma psi_phi1 a b (c:= psi_phi_aux a b): c < phi a c.
proof: Proof. move: (phi_ab_le1 a c); case /orP => // /eqP h. symmetry in h;move: (phi_fix2 h). case aux: (b == [T2_pr1 b, T2_pr2 b]). case h1: ([T2_pr1 b, T2_pr2 b] == one). rewrite /c /psi_phi_aux (eqP aux) /= h1 /=. by move => /= [pa]; move: (eqP h1) => [->]; rewrite T2ltn0. move: (erefl c); rewrite {2} /c /psi_phi_aux (eqP aux) /= h1 - (eqP aux). case h2: (phi a b == b); first by move => ->; case. by move => e1 _; move: h2; rewrite - e1 h eqxx. rewrite /c /psi_phi_aux; case: (T2split b) => u _. case h1: (phi a u == u); last by move => [h2 _]; move: aux; rewrite - h2 eqxx. case; case b => //; first by rewrite T2ltn0. move => a1 b1 n1 c1 /=. case h2: ([a1, b1] == one) => /=; first by rewrite T2ltn0. by case => _ h3; move: (succ_nz c1); rewrite h3. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)