proposition: Lemma util_C : forall n i j : nat, (i <= j)%nat -> (j <= n)%nat -> ('C(n, i) * 'C(n-i, j-i) = 'C(j, i) * 'C(n, j))%nat.
proof: Proof. move => n i j ij jn. apply/eqP; rewrite -(@eqn_pmul2r ( i`! * (n - i) `!)); last by rewrite muln_gt0; apply/andP; split; apply: fact_gt0. rewrite -(@eqn_pmul2r ((j - i)`! * ((n - i)-(j - i))`!)); last first. by rewrite muln_gt0; apply/andP; split; apply: fact_gt0. have ilen : (i <= n)%nat by apply: leq_trans jn. rewrite (mulnAC 'C(n, i)) -mulnA !bin_fact //; last by apply: leq_sub2r. rewrite !mulnA (mulnAC _ _ (i`!)) 2!(mulnAC _ _ ((j-i)`!)) -(mulnA 'C(j, i)). rewrite bin_fact // -subnDA subnKC // mulnAC (mulnC j`!) -(mulnA _ j`!). by rewrite bin_fact. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc