proposition: Lemma finite_intersections_len_S_exists {X : Type} {F : Family X} {U : Ensemble X} {n : nat} : In (finite_intersections_len F (S n)) U -> exists V W, In (finite_intersections_len F n) V /\ In (finite_intersections_len F 1) W /\ U = Intersection V W.
proof: Proof. generalize dependent U. generalize dependent n. apply (well_founded_ind Wf_nat.lt_wf (fun n => forall U, In (finite_intersections_len F (S n)) U -> exists V W, In (finite_intersections_len F n) V /\ In (finite_intersections_len F 1) W /\ U = Intersection V W)). intros [|n] IH U H. - apply finite_intersections_len_1_in in H. exists Full_set, U. now repeat split; constructor + rewrite Intersection_Full_set. - apply finite_intersections_len_SS_intersection in H. destruct H as [m [[|k] [V [W [HV [HW [eq1 eq2]]]]]]]. + rewrite PeanoNat.Nat.add_0_r in eq2. subst. now exists V, W. + apply IH in HV; [|lia]. destruct HV as [V1 [V2 [HV1 [HV2 eq3]]]]. rewrite eq2, plus_n_Sm. exists (Intersection V1 W), V2. repeat (constructor; try easy). subst. now rewrite (Intersection_associative V1 W), (Intersection_commutative _ W), <- (Intersection_associative V1). Qed.
imports: Coq(ClassicalChoice Lia Program.Equality) ZornsLemma(EnsemblesImplicit InverseImage Proj1SigInjective)