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