proposition: Lemma phi_fix2 a b (u:= T2_pr1 b) (v:= T2_pr2 b): phi a b = b -> b = [u,v] /\ a < u.
proof: Proof. move => h. split; first by rewrite -h phi_ap h. move: (h). rewrite - h (phi_ap a b) h -/u -/v /=. by case: (a <u) => // h1; move: (T2lt_psi_b a [u, v]); rewrite h1 T2ltnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)