proposition: Lemma Nintcc_exten_spec q i j: natp q -> natp i -> Nintcc i (i +c (q -c \1c)) = Nintcc j (j +c (q -c \1c)) -> i = j.
proof: Proof. move => qN iN eqa. have la: i <=c (i +c (q -c \1c)) by apply:csum_M0le; fprops. have bN: natp (i +c (q -c \1c)) by apply: (NS_sum iN (NS_diff _ qN)). exact: (proj1 (Nintcc_exten la bN eqa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)