proposition: Lemma sub1a x: x != zero -> T3nf x -> x = one + (x - one).
proof: Proof. case fb:(T3finite x); last by rewrite sub1Nfin ?fb // add1Nfin // fb //. move: fb;case x => // a' b' c' n' d' /=. rewrite all_zeroE T3lt1 T3gt1 /= => h _; rewrite h (eqP h) T3lt1 /=. by move: (eqP h); case => -> -> ->; move /and5P=> [_ _ _ _ /eqP -> ];case n'. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)