proposition: Lemma Ex6_32p2 n f: intp n -> csumb (ZN_int n \0c \1c) f = f n +c f (BZsucc n).
proof: Proof. move => nz. have h: ~ inc (BZsucc n) (singleton n). by move:(nesym (proj2 (zlt_succ nz))) => /set1_P. by rewrite(Ex6_32p1 nz) - setU2_11 (csumA_setU1 _ h) csum_trivial3 csum2cl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)