proposition: Lemma phi_ap x y : (phi x y) = [T2_pr1 (phi x y), T2_pr2 (phi x y)].
proof: Proof. case: y => // a b n c /=. case h: (_ && _) => //; last by case: (_ && _). by case (x < a) => /=; move/andP: h => [/eqP -> /eqP ->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)