proposition: Lemma succ_lt a: a < T2succ a.
proof: Proof. elim: a => // a _ b _ n c Hc /=; case pa: ([a, b] == one). by move: (eqP pa) => [-> ->]; rewrite T2lt_consE ltnSn. by rewrite T2lt_consE !eqxx Hc !if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)