proposition: Lemma mapmult_image : forall (a : Z) (l : Zlist) (x : Z), inlist Z x l -> inlist Z (a * x)%Z (mapmult a l).
proof: Proof. unfold mapmult in |- *. unfold inlist in |- *. simple induction l. simpl in |- *. intros. assumption. simpl in |- *. intros h t IH. intros. elim H. left. rewrite H0. reflexivity. right. apply IH. assumption. Qed.
imports: Arith ZArith EqNat dec natZ