proposition: Lemma ZN_ointP n a b: intp n -> natp a -> natp b -> forall x, inc x (ZN_oint n a b) <-> zbetween x (n -z (ZN a))(n +z (ZN b)).
proof: Proof. move => nz aN bN x. move: BZor_or BZor_sr => or sr. rewrite /ZN_oint /interval_co sr. split; first by move/Zo_hi => [/zle_P ha /zlt_P hb]. move =>[le1 le2]; move: (proj31_1 le2) => xz; apply: (Zo_i xz). by split; [apply/zle_P | apply /zlt_P]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)