proposition: Lemma total_order_from_list_filterP A l (P : A -> Prop): total_order_from_list (filterP P l) ≡ total_order_from_list l ∩ P × P.
proof: Proof. unfold inter_rel, cross_rel. split; red; induction l as [ | a l]; ins; desf. all: try solve [forward eapply total_order_from_list_in1; eauto; ins]. all: repeat rewrite total_order_from_list_cons in *; desf. all: try rewrite in_filterP_iff in *; desf; eauto. all: try apply IHl in H; desf; eauto. Qed.
imports: HahnBase HahnList HahnRelationsBasic