proposition: Lemma ex4_propc1: nonempty (projective_limit ex4_system) -> exists2 s, countable_set s & cofinal r s.
proof: Proof. by move => [x /ex4_propc []]; set s:= fun_image _ _ => ha hb; exists s. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)