proposition: Lemma bin_fact2n_b n : 0<n -> 'C(n.*2, n.-1) * (n`! * n.+1`!) = (n.*2)`!*n.
proof: Proof. case: n => // n _ /=. rewrite factSr mulnAC mulnA. by move:(bin_fact (leq_addr n.+2 n)); rewrite addKn - addSnnS addnn => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)