Add results about trace.

Lebesgue/Set_theory/Set_seq.v

@@ -1211,6 +1211,28 @@ Proof.
 intros; rewrite union_seq_unionf_any_double, union_seq_double; easy.
 Qed.
 
+Lemma trace_incr_seq :
+  forall (A : set U) (B : nat -> set U),
+    incr_seq B -> incr_seq (tracem_seq A B).
+Proof.
+intros A B HB n; apply trace_monot; easy.
+Qed.
+
+Lemma trace_decr_seq :
+  forall (A : set U) (B : nat -> set U),
+    decr_seq B -> decr_seq (tracem_seq A B).
+Proof.
+intros A B HB n; apply trace_monot; easy.
+Qed.
+
+Lemma trace_disj_seq :
+  forall (A : set U) (B : nat -> set U),
+    disj_seq B -> disj_seq (tracem_seq A B).
+Proof.
+intros A B HB n1 n2 Hn [x HAx] Hx1 Hx2.
+apply (HB _ _ Hn x); easy.
+Qed.
+
 (* Useful? *)
 Lemma trace_union_seq :
   forall (A : set U) (B : nat -> set U),