proposition: Lemma cdiff_lt_symmetry' n p: natp p -> p <> \0c -> cpred (p -c n) <c p.
proof: Proof. move=> pN pnz. exact: (cle_ltT (cpred_monotone (cdiff_le1 n (CS_nat pN))) (cpred_lt pN pnz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)