proposition: Lemma mapmult_orig : forall (a : Z) (l : Zlist) (y : Z), inlist Z y (mapmult a l) -> exists x : Z, inlist Z x l /\ y = (a * x)%Z.
proof: Proof. unfold mapmult in |- *. unfold inlist in |- *. simple induction l. simpl in |- *. intros. elim H. simpl in |- *. intros h t IH. intros. elim H. intro. split with h. split. left. reflexivity. assumption. intro. elim (IH y). intros. elim H1. intros. split with x. split. right. assumption. assumption. assumption. Qed.
imports: Arith ZArith EqNat dec natZ