proposition: Lemma mkmult_rec_ok : forall lm r, mkmult_rec r lm == r * r_list_pow lm.
proof: Proof. intros lm; induction lm as [|a lm IHlm];intros;simpl;Esimpl. destruct a as (x,p);Esimpl. rewrite IHlm. rewrite mkmult_pow_spec. Esimpl. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory