proposition: Fact cdM (n : nat) (k m : int) : 0 <= k -> 1 <= m -> m < k + 1 -> k < Posz n + 1 -> c n k * d n k m = ((-1) ^ (m + 1) / 2%:Q) / (m%:Q ^ 3 * (binomialz k m)%:Q ^ 2) * (binomialz n k * binomialz (Posz n + k) k * binomialz (Posz n - m) (Posz n - k) * binomialz ((Posz n) + k) (k - m))%:Q.
proof: Proof. case: m k => m // [] // k _ h1m. rewrite /c /d -!PoszD !addn1 !ltz_nat !ltnS !rmorphM /= => hmk hkn. have hnm : (m <= n)%N by lia. rewrite (subzn hkn) (subzn hmk) (subzn hnm) !binzE; [| lia..]. have -> : (n + k - (k - m) = n + m)%N by rewrite subnBA // addnAC addnK. have -> : (n - m - (n - k) = k - m)%N by rewrite subnAC subnBA // addKn. rewrite !addnK; field. rewrite !pnatr_eq0 -!lt0n !fact_gt0; lia. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics binomialz bigopz arithmetics seq_defs a_props