proposition: Lemma prl_exa3_prop7: projective_limit prl_exa3_system = emptyset.
proof: Proof. apply/set0_P => t /prl_exa3_prop6 [ha hb]. move:(hb _ (NS_succ ha)); set x := Vg _ _; set y := Vg _ _ => eqa. move:(csum_Mle0 y (CS_succ x)); rewrite - eqa => le1. by move:(cltNge (cltS ha) le1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)