proposition: Lemma phi_le3 a b: a < T2_pr1 (phi a b) -> (phi a b) = b.
proof: Proof. case:b; first by rewrite /= T2ltnn. move => a'' b'' n'' c'' /=. case sa: (_ && _); first by case aa: (a < a'') => //=; rewrite T2ltnn. by case sb: (_ && _) => //=; rewrite T2ltnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)