fact: Fixpoint mkmult_rec (r:R) (lm:list (R*positive)) {struct lm}: R := match lm with | nil => r | cons (x,p) t => mkmult_rec (mkmult_pow r x p) t end.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory