proposition: Lemma inf_Nat E (x:= intersection E): sub E Nat -> nonempty E -> inc x E /\ (forall y, inc y E -> x <=c y).
proof: Proof. by move => pa; apply:cle_wor' => // t /pa /CS_nat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)