proposition: Lemma sub1a x: x != zero -> T2nf x -> x = one + (x - one).
proof: Proof. case fb:(T2finite x); last by rewrite sub1Nfin ?fb // add1Nfin // fb //. move: fb;case x => // a' b' n' c' /=. rewrite T2lt1 T2gt1 T2eqE andbT/= => /andP [/eqP -> /eqP ->] _. by rewrite T2lt1 /= => /andP [_ /eqP ->];case n'. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)