Add trace_monot.

Lebesgue/Set_theory/Set_base.v

@@ -2151,6 +2151,12 @@ intros A B; rewrite 2!full_equiv.
 intros HB; rewrite HB; apply trace_fullset_r.
 Qed.
 
+Lemma trace_monot :
+  forall (A B1 B2 : set U), incl B1 B2 -> incl (trace A B1) (trace A B2).
+Proof.
+intros A B1 B2 HB x Hx; apply HB; easy.
+Qed.
+
 (* Useful? *)
 Lemma trace_compl :
   forall (A B : set U), trace A (compl B) = compl (trace A B).