proposition: Lemma succ_lt a: a < T3succ a.
proof: Proof. elim: a => // a _ b _ c _ n d Hd /=; rewrite all_zeroE; case: eqP. by rewrite T3lt_consE ltnS leqnn; move => ->; rewrite T3ltnn eqxx. by rewrite T3lt_consE !eqxx Hd !if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)