proposition: Lemma union_wo: well_ordered union.
proof: Proof. assert (total: ∀ x y : A, x ∈ union → y ∈ union → x ≼ y ∨ y ≼ x). { intros ?? [Sx [inSx inx]] [Sy [inSy iny]]. destruct (chain Sx Sy) as [[sub _]|[sub _]]; auto; [apply (wo_total Sy)|apply (wo_total Sx)]; auto. } split; trivial. intros ? sub [y inh]. destruct (sub y inh) as [Sy [inSy iny]]. assert (Proper (equ ==> iff) (λ x, x ∈ Y ∧ x ∈ Sy)) as inter_spec by solve_proper. set (exist _ _ inter_spec) as inter. destruct (wo_minima Sy (wo Sy inSy) inter) as [m [[inm inm'] min]]; [firstorder..|]. exists m; split; auto. intros x inx. destruct (sub x inx) as [Z [inSz inx']]. destruct (chain Sy Z) as [[sub' cl']|[??]]; eauto; [|apply min; split; auto]. destruct (total m x) as [case|case]; [apply sub; trivial..|auto|]. apply cl' in case; auto. apply min; split; auto. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)