proposition: Lemma U_nkbin_pr n k : n * 'C(n+k,k.*2.+1) = (k.+1) * (U_nkbin n k).
proof: Proof. rewrite /U_nkbin (binS _ k.*2.+1) addnA addnn mulnDr. rewrite -(mul2n 'C(_,_)) mulnA mulSnr muln2 addn2 - mul_Sm_binm_2 - mulnDl. rewrite - {2} addnn -addnS subnDA addnK -addnn - addSn. by case (leqP k.+1 n) => h; rewrite ?(subnK h) // bin_small ? ltn_add2r ?muln0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)