proposition: Lemma binom_exchange j k q : 'C(j + k + q, j + k) * 'C(j + k, j) = 'C(k + q, k) * 'C(j + k + q, j).
proof: Proof. have bin_fact1: forall n m, 'C(n+m,m) * (m`! * n`!) = (n+m)`!. by move => n m; move: (bin_fact (leq_addl n m)); rewrite addnK. move: (bin_fact1 (k+q) j) (bin_fact1 q (j+k)). rewrite (mulnC j`!) (addnC k)(addnC j) - (bin_fact1 q k) - (bin_fact1 k j). rewrite (mulnAC _ _ j`!) !mulnA - (addnA q) (addnC q) => <-. move /eqP; rewrite !eqn_pmul2r ? fact_gt0 //;move /eqP ->; apply: mulnC. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)