proposition: Lemma succ_pred x: T2nf x -> T2is_succ x -> x = T2succ (T2pred x).
proof: Proof. elim:x => // a _ b _ n c Hc nf /=. case az: ([a, b] == one) => /=. rewrite (T2nf_finite az nf); move: (eqP az) => [-> ->]; case n => //. by rewrite az => h; rewrite - Hc //; case/and4P: nf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)