proposition: Lemma ex4d (S:= (ex4_system (proj1 ex4d_orderIr_prop3))): [/\ (forall i, inc i (psI S) -> nonempty (Vg (psE S) i)), (forall ij, inc ij (psr S) -> surjection (Vg (psf S) ij)) & (projective_limit S) = emptyset].
proof: Proof. case:(ex4_system_prop (proj1 ex4d_orderIr_prop3)). set Hu := (proj1 ex4d_orderIr_prop3). rewrite -/S; move => s_E s_I s_r s_f. rewrite s_I s_r s_E s_f; split => //. - by move => i iI; rewrite LgV//; apply:ex4_setEi_nonempty. - move => ij ijr; rewrite/ex4_function_f_fam LgV//. have pp: pairp ij by move: (Hu) => [_ /order_sgraph sg _ _ _ ]; apply: sg. rewrite - pp in ijr |- *. exact:(ex4_function_f_sf Hu ijr). - case: (emptyset_dichot (projective_limit S)) => // le. move:(ex4_propc1 le) => [s sa sb]. case: (proj2 ex4d_orderIr_prop3 _ sb sa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)