proposition: Lemma phi_ab_le1 a b: b <= phi a b.
proof: Proof. case:(phi_cases a b). case; move => -> //; apply: T2ltW; apply: T2lt_psi_b. move => [sa sb];rewrite sa {1} sb. apply: T2le_psi_b. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)