proposition: Lemma bin_fact2n_c n :'C(n.*2, n) * (n`! * n.+1`!) = (n.*2)`!*n.+1.
proof: Proof. by rewrite factSr (mulnA n`!) mulnn mulnA bin_fact2n_a. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)