proposition: Lemma comb_expE (rR : realDomainType): (comb_exp (1 : rR) = 1%N) * (comb_exp (-1 : rR) = 2%N) * (comb_exp (0 : rR) = 0%N).
proof: Proof. by rewrite /comb_exp sgzN sgz1 sgz0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)