proposition: Lemma phi_mono_b a b b': T2nf b -> b <= b' -> phi a b <= phi a b'.
proof: Proof. move => sb. by case /orP; [move => /eqP -> |move => sd;apply:T2ltW;apply:phi_mono_a]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)