proposition: Lemma multdrop_cons_neq : forall (p q : nat) (l : natlist), p <> q -> multDrop p (Cons nat q l) = q * multDrop p l.
proof: Proof. unfold multDrop in |- *. simpl in |- *. intros. elim (beq_nat_neq p q). intros. rewrite H0. simpl in |- *. reflexivity. assumption. Qed.
imports: Arith ZArith EqNat dec natZ