proposition: Lemma ZN_intP n a b: intp n -> natp a -> natp b -> forall x, inc x (ZN_int n a b) <-> zbetween_eq 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_int /interval_cc sr. split; first by move/Zo_hi => [/zle_P ha /zle_P hb]. move =>[le1 le2]. by move: (proj31 le2) => xz;apply: (Zo_i xz); split; apply/zle_P. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)