Add compatibility of Trace with (finite) set systems.

Lebesgue/Set_theory/Set_system/Set_system_finite.v

@@ -871,3 +871,34 @@ rewrite (set_ext (prop_cst P) emptyset); [apply Algebra_wEmpty | easy].
 Qed.
 
 End More_Facts.
+
+
+Section Trace_Facts.
+
+Context {U : Type}.
+Variable P : set_system U.
+Variable A0 V : set U.
+
+Lemma Trace_Psyst : is_Psyst P A0 -> is_Psyst (Trace P V) (trace V A0).
+Proof.
+rewrite 2!Psyst_equiv; intros [HP1 HP2]; split; try easy.
+apply Trace_Inter; easy.
+Qed.
+
+Lemma Trace_Ring : is_Ring P -> is_Ring (Trace P V).
+Proof.
+rewrite 2!Ring_equiv; intros [HP1 [HP2 HP3]]; repeat split.
+apply Trace_wEmpty; easy.
+apply Trace_Diff; easy.
+apply Trace_Union; easy.
+Qed.
+
+Lemma Trace_Algebra : is_Algebra P -> is_Algebra (Trace P V).
+Proof.
+rewrite 2!Algebra_equiv; intros [HP1 [HP2 HP3]]; repeat split.
+apply Trace_wEmpty; easy.
+apply Trace_Compl; easy.
+apply Trace_Union; easy.
+Qed.
+
+End Trace_Facts.