proposition: Lemma succ_pred x: T3nf x -> T3is_succ x -> x = T3succ (T3pred x).
proof: Proof. elim:x => // a _ b _ c _ n d Hd /= /and5P [pa pb pc pd pe]. case az: (all_zero a b c) => /=; last by rewrite az => h; rewrite - Hd. move: pe;move/and3P: az=> [/eqP -> /eqP -> /eqP ->]. by rewrite T3lt1 => /eqP ->; case:n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)