proposition: Lemma Ex59_intp q i: natp q -> \0c <c q -> natp i -> i +c q = csucc (i +c (q -c \1c)).
proof: Proof. move => qN qp iN. have sb': \1c <=c q by apply/cge1P. have dN:=(NS_diff \1c qN). have cq:cardinalp (q -c \1c) by apply:CS_diff. by rewrite - (csum_nS _ dN) (csucc_pr4 cq) (csumC _ \1c) (cdiff_pr sb'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)