proposition: Lemma phi_le1 a b: a <= T2_pr1 (phi a b).
proof: Proof. case:b; first by rewrite /= T2lenn. move => a'' b'' n'' c'' /=; rewrite !fun_if /= eqxx if_same. by case: (a < a''); rewrite !if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)