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