proposition: Lemma all_ge0_cat {R'' : realDomainType} : {morph (@all_ge0 R'') : x y / x ++ y >-> x && y}.
proof: Proof. by elim=> [ | a x IH y] //=; rewrite IH andbA. 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