proposition: Lemma sub1a x: x != zero -> T1nf x -> x = one + (x - one).
proof: Proof. move => na nb;case fb:(T1finite x). move: na fb nb ; case: x => // a' n' b' /= _ /eqP ->. by rewrite T1lt1 => /and3P [_ _ /eqP ->]; case: n'. rewrite sub1Nfin ?fb // add1Nfin // fb //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)