proposition: Lemma phi_le2 a b: T2_pr2 (phi a b) <= b.
proof: Proof. case:b; first by rewrite /= T2lenn. move => a'' b'' n'' c'' /=. case sa: (_ && _). case aa: (a < a'') => //=. apply: T2le_trans (T2le_psi1 a'' b'' n'' c''). apply /T2ltW; apply:T2lt_psi_b. case sb: (_ && _) => //=; rewrite T2le_consE pred_le !eqxx /=. by case n'' => //=; rewrite if_same //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)