WIP: "seq" results about Trace.

Lebesgue/Set_theory/Set_system/Set_system_base_seq.v

@@ -379,14 +379,43 @@ Qed.
 
 Lemma Trace_Inter_monot_seq : Inter_monot_seq P -> Inter_monot_seq (Trace P V).
 Proof.
+intros HP A HA1 HA2.
+assert (HA3 : forall n, exists B, P B /\ A n = trace V B).
+  intros n; induction (HA2 n) as [B HB]; exists B; easy.
+destruct (choice _ HA3) as [B HB1].
+assert (HB2 : decr_seq B).
+  intros n. admit.
+replace (inter_seq A) with (inter_seq (tracem_seq V B)).
+rewrite <- trace_inter_seq; apply Tr, HP; try apply HB1; easy.
+apply inter_seq_ext; intros n; symmetry; apply HB1.
 Admitted.
 
 Lemma Trace_Union_monot_seq : Union_monot_seq P -> Union_monot_seq (Trace P V).
 Proof.
+intros HP A HA1 HA2.
+assert (HA3 : forall n, exists B, P B /\ A n = trace V B).
+  intros n; induction (HA2 n) as [B HB]; exists B; easy.
+destruct (choice _ HA3) as [B HB1].
+assert (HB2 : incr_seq B).
+  intros n. admit.
+replace (union_seq A) with (union_seq (tracem_seq V B)).
+rewrite <- trace_union_seq; apply Tr, HP; try apply HB1; easy.
+apply union_seq_ext; intros n; symmetry; apply HB1.
 Admitted.
 
 Lemma Trace_Union_disj_seq : Union_disj_seq P -> Union_disj_seq (Trace P V).
 Proof.
+intros HP A HA1 HA2.
+assert (HA3 : forall n, exists B, P B /\ A n = trace V B).
+  intros n; induction (HA2 n) as [B HB]; exists B; easy.
+destruct (choice _ HA3) as [B HB1].
+assert (HB2 : disj_seq B).
+  intros n1 n2 Hn.
+
+ admit.
+replace (union_seq A) with (union_seq (tracem_seq V B)).
+rewrite <- trace_union_seq; apply Tr, HP; try apply HB1; easy.
+apply union_seq_ext; intros n; symmetry; apply HB1.
 Admitted.
 
 End Seq_Facts3.