proposition: Lemma cons_poly_add {R: ringType} (m m': R) (q1 q2: {poly R}): (cons_poly m' (q1 + q2) = (cons_poly m q1) + cons_poly (m'-m) q2)%R.
proof: Proof. apply coef_poly_eq => i. rewrite coefD !coef_cons coefD. case: i => //=. by rewrite GRing.addrC -GRing.addrA GRing.addNr GRing.addr0. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude) extructures(ord fset fmap) Equations(Equations)