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