add lemmas about seq

Adding a couple of lemmas about seq. Please let me know if you prefer bigger MRs. I have a fair amount of stuff that I want to merge eventually.

stdpp/list_numbers.v

@@ -98,6 +98,16 @@ Section seq.
     k ∈ seq j n ↔ j ≤ k < j + n.
   Proof. rewrite elem_of_list_In, in_seq. done. Qed.
 
+  Lemma seq_nil n m:
+  seq n m = [] ↔
+  m = 0.
+  Proof. by induction n; induction m. Qed.
+
+  Lemma seq_subseteq m n1 n2 :
+    n1 ≤ n2 →
+    seq m n1 ⊆ seq m n2.
+  Proof. by intros Hle i Hi%elem_of_seq; apply elem_of_seq; lia. Qed.
+
   Lemma Forall_seq (P : nat → Prop) i n :
     Forall P (seq i n) ↔ ∀ j, i ≤ j < i + n → P j.
   Proof. rewrite Forall_forall. setoid_rewrite elem_of_seq. auto with lia. Qed.
@@ -118,6 +128,7 @@ Section seq.
     - rewrite take_nil. replace (m `min` 0) with 0 by lia. done.
     - destruct m; simpl; auto with f_equal.
   Qed.
+
 End seq.
 
 (** ** Properties of the [seqZ] function *)