proposition: Lemma phi_eqE a b a' b': T2nf a -> T2nf a' -> T2nf b -> T2nf b' -> (phi a b == phi a' b') = (if a < a' then b == phi a' b' else if a' < a then phi a b == b' else b== b').
proof: Proof. move => na na' nb nb'. case: (T2ltgtP a a') => h. + move: (T2lt_le_trans h (phi_le1 a' b')) => sa. have sb: phi a (phi a' b') = phi a' b' by rewrite (phi_ap a' b') /= sa. by rewrite - {1} sb; apply: phi_inj1 => //; apply: nf_phi. + move: (T2lt_le_trans h (phi_le1 a b)) => sa. have sb: phi a' (phi a b) = phi a b by rewrite (phi_ap a b) /= sa. by rewrite - {1} sb; apply: phi_inj1 => //; apply: nf_phi. + by rewrite h;apply: phi_inj1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)