proposition: Lemma phi_spec4b x: phi zero x = x -> x = [T2_pr1 x, T2_pr2 x] /\ T2_pr1 x != zero.
proof: Proof. by move /phi_fix2; rewrite T2lt0n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)