proposition: Lemma T3nf_finite a b c n d: all_zero a b c -> T3nf (cons a b c n d) -> d = zero.
proof: Proof. move => /and3P [/eqP -> /eqP ->] /eqP -> /and5P [_ _ _ _]. by rewrite T3lt1 => /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)