proposition: Lemma phi_ab_le2 a b:a < phi a b.
proof: Proof. case:(phi_cases a b). case => h; last by rewrite h; apply: T2lt_psi_a. move:(phi_fix2 h) => [sa sb]. by apply: (T2lt_trans sb); rewrite h {2} sa; apply: T2lt_psi_a. move => [-> _]; apply: T2lt_psi_a. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)