proposition: Lemma phi_mono_c a b b': T2nf b -> T2nf b' -> (phi a b < phi a b') = (b < b').
proof: Proof. move => sa sb; case: (T2ltP b b') => // h; first exact:(phi_mono_a a sa h). by rewrite T2ltNge phi_mono_b. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)