proposition: Lemma phi_inj a b b': T2nf b -> T2nf b' -> phi a b = phi a b' -> b = b'.
proof: Proof. move => pa pb pc; case: (T2ltgtP b b') => // h. by move: (phi_mono_a a pa h); rewrite pc T2ltnn. by move: (phi_mono_a a pb h); rewrite pc T2ltnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)