proposition: Lemma nonempty_le: forall N1 N2, le N1 N2 -> isempty N1 = false -> (Zinf.le (high N1) (high N2) /\ Zinf.le (low N1) (low N2)).
proof: Proof. unfold le, In, isempty; intros. destruct N1 as [[l1 |] [h1|]]; cbn in *; rewrite ? Zinf.le_Fin, ? Zinf.le_Inf. - apply Z.ltb_ge in H0. split. + apply H; lia. + replace l1 with (- - l1) by lia. apply H. lia. - split. + apply Zinf.le_is_Inf with (-l1). intros; apply H. intuition lia. + replace l1 with (- - l1) by lia. apply H. intuition lia. - split. + apply H. intuition lia. + apply Zinf.le_is_Inf with(- h1). intros. replace n with (- - n) by lia. apply H. intuition lia. - split; apply Zinf.le_is_Inf with 0; intros. + apply H; auto. + replace n with (- - n) by lia. apply H. auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)