proposition: Lemma multdrop_mult : forall (qlist : natlist) (q : nat), inlist nat q qlist -> q * multDrop q qlist = product qlist.
proof: Proof. simple induction qlist. simpl in |- *. intros. elim H. simpl in |- *. intros q1 l IH. intros. elim (eqdec q q1). intro. rewrite H0. rewrite multdrop_cons_eq. reflexivity. intro. rewrite multdrop_cons_neq. rewrite <- (IH q). rewrite mult_assoc. rewrite (mult_comm q q1). rewrite mult_assoc. reflexivity. unfold inlist in H. simpl in H. elim H. intro. elim H0. assumption. intro. assumption. assumption. Qed.
imports: Arith ZArith EqNat dec natZ