proposition: Lemma isempty_2: forall N, isempty N = false -> exists n, In n N.
proof: Proof. unfold isempty, In; intros. destruct N as [[l|] [h|]]; cbn. - apply Z.ltb_ge in H. exists h; lia. - exists (- l); lia. - exists h; lia. - exists 0; auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)