coq中的自然数列表

Question

我正在写关于natlist（l）长度的引理，引理的陈述是“ l的长度等于零给出假”（长度l =？0）= false。仅当列表的头部，头部和尾部或空的[[]列表从不出现时，才有可能。请帮助我在Proposition中编写此语句。 _->（长度l =？0）= false。

Answer 1

forall l : natlist, l <> [] -> (length l =? 0) = false呢？