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