proposition: Lemma Exercise5_9l5 J x: Ex59_pos_in_J J \0c x = \0c.
proof: Proof. rewrite /Ex59_pos_in_J Nint_co00; set y := Zo _ _. have ->: y = emptyset by apply/set0_P => t / Zo_S /in_set0. by rewrite set0_U2 setI_1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)