proposition: Lemma mkVmon_ok M i l : (mkVmon i M)@@l == M@@l * (hd l)^i.
proof: Proof. destruct M;simpl;intros;rsimpl. - rewrite zmon_pred_ok;simpl;rsimpl. - rewrite pow_pos_add;rsimpl. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory