proposition: Lemma mkmult1_ok : forall lm, mkmult1 lm == r_list_pow lm.
proof: Proof. intros lm; destruct lm as [|p lm];simpl;Esimpl. destruct p. rewrite mkmult_rec_ok;rewrite mkpow_spec;Esimpl. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory