proposition: Lemma sub_nz a b: T2nf b -> a < b -> (b - a) != zero.
proof: Proof. move => nb lab; move: (sub_pr1 nb (T2ltW lab)). case h: (b - a == zero) => //; rewrite (eqP h) T2addn0 => eq. by move: lab; rewrite eq T2ltnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)