proposition: Lemma Zermelo_chain_least E F: Zermelo_chain E F -> inc emptyset F.
proof: Proof. move => [pa pb pc pd]. have nef: nonempty F by exists E; apply: pb. move: (pd _ (@sub_refl F) nef); set x := intersection F => iF. case: (emptyset_dichot x); [by move <- | move => xne]. move: (pc _ iF) => siF. by move: (setI_hi (rep_i xne) siF) => /setC1_P []. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)