proposition: Lemma NS_inf_Nat E (x:= intersection E): sub E Nat -> natp x.
proof: Proof. move => h; case (emptyset_dichot E) => h1. rewrite /x h1 setI_0; fprops. exact: (h _ (proj1 (inf_Nat h h1))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)