proposition: Lemma Ex6_32p1 n: intp n -> ZN_int n \0c \1c = doubleton n (BZsucc n).
proof: Proof. move => nz. move: (ZN_intP nz NS0 NS1); rewrite (Ex6_32p0 nz) => H. move: (proj1 (zlt_succ nz)) => la. set_extens t. move/H =>[ha hb]; case: (equal_or_not t (BZsucc n)) => ee. rewrite ee; apply: set2_2. move/(zlt_succ1P (proj32 ha) (proj31 ha)): (conj hb ee) => ltn. by rewrite - (zleA ha ltn); apply: set2_1. case/set2_P => ->. by apply/H; split => //; apply:(zleR nz). by apply/H; split => //; apply: (zleR (ZS_succ nz)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)