proposition: Lemma sub1b x: T2nf x -> x = (one + x) - one.
proof: Proof. case h: (T2finite x); last by rewrite add1Nfin ? h // sub1Nfin // h. by move => nx; rewrite (T2finite2 h nx); case: (T2split x).2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)