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