proposition: Lemma binom_symmetric2 n m: natp n -> natp m -> binom (n +c m) m = binom (n +c m) n.
proof: Proof. move => nN mN. rewrite csumC (binom_symmetric (NS_sum mN nN) (Nsum_M0le n mN)). rewrite csumC (cdiff_pr1 nN mN) //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)