proposition: Lemma Cauchy_kernel_coeff_symmetric mon : (Cauchy_kernel d)@_mon \is symmetric.
proof: Proof. rewrite Cauchy_symm_symh linear_sum /=; apply rpred_sum => la _. rewrite linearZ /= rpredM ?sympolP //. case: (ssrnat.leqP (size la) m) => [/mcoeff_symm -> | /symm_oversize ->]. - by case: (perm_eq _ _) => /=; [exact: rpred1 | exact: rpred0]. - by rewrite mcoeff0 rpred0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssrint rat ssralg ssrnum algC matrix vector) mathcomp(mpoly) tools partition ordtype antisym Schur_mpoly Schur_altdef sympoly homogsym permcent