proposition: Lemma sub_nz a b: T1nf b -> a < b -> (b - a) != zero.
proof: Proof. move => nb lab; apply/negP => h. by move: (sub_pr1r nb (eqP h)); rewrite T1leNgt lab. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)