proposition: Lemma cpred_pr4 a: cardinalp a -> cpred a = a -c \1c.
proof: Proof. move=> ca. case: (Nat_dichot ca) => aN. case: (equal_or_not a \0c) => anz. by rewrite anz cpred0 (cdiff_wrong cle_01). move:(cpred_pr aN anz) => [sa {2} ->]. by rewrite (csucc_pr4 (CS_nat sa)) (cdiff_pr1 sa NS1). by rewrite (cpred_inf aN) (cdiff_fin_infin finite_1 aN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)