proposition: Lemma mkadd_mult_ok : forall rP c lm, mkadd_mult rP c lm == rP + [c]*r_list_pow lm.
proof: Proof. intros rP c lm;unfold mkadd_mult. case_eq (get_sign c);intros c0; try intros H. - rewrite (morph_eq CRmorph _ _ (sign_spec get_sign_spec _ H));Esimpl. rewrite mkmult_c_pos_ok;Esimpl. - rewrite mkmult_c_pos_ok;Esimpl. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory