proposition: Lemma bin_fact2n_f n: 0 <n -> 'C(n.*2.+2, n.+1) - 'C(n.*2.+2, n) = 'C(n.*2.+1, n.+1) - 'C(n.*2.+1, n.-1).
proof: Proof. move => h; have eqa:= (prednK h). by rewrite -{4} eqa binS (binS n.*2.+1) eqa addnC subnDl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)