proposition: Lemma Ex59_interval_prop q j: natp j -> natp q -> \0c <c q -> forall x, inc x (Nintcc j (j +c (q -c \1c))) <-> j <=c x /\ x <c j +c q.
proof: Proof. move => jN qN qp x. have sdN:= NS_sum jN (NS_diff \1c qN). rewrite (Ex59_intp qN qp jN). split. by move/Nint_ccP => [[xN _ la] [_ _ lb]]; split => //;apply/(cltSleP sdN). move => [la /(cltSleP sdN) lb]. by have xN := NS_le_nat lb sdN; apply/Nint_ccP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)