proposition: Lemma nf_consE a b c n d: T3nf (cons a b c n d) = [&& T3nf [a,b,c], T3nf d & d < [a,b,c] ].
proof: Proof. by rewrite /T3nf -/T3nf T3lt0n /= andbT !andbA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)