proposition: Lemma add_pow_list_ok : forall r n l, r_list_pow (add_pow_list r n l) == pow_N rI rmul r n * r_list_pow l.
proof: Proof. intros r n; destruct n;simpl;intros;Esimpl. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory