proposition: Lemma succ_p1 x: T3is_succ (T3succ x).
proof: Proof. elim: x => // a _ b _ c _ n d Hd /=. by case: (all_zero a b c) => //=;rewrite Hd orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)