proposition: Lemma T2nf_finite a b n c: [a,b]==one -> T2nf (cons a b n c) -> c = zero.
proof: Proof. by move => /eqP [-> ->] /and4P [_ _ _]; rewrite T2lt1 => /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)