proposition: Lemma sub1Nfin a: ~~ T2finite a -> a - one = a.
proof: Proof. by case:a => // a b n c /=; rewrite T2lt1 T2gt1 T2eqE andbT => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)