Removing the same item added to a given multiset (AKA bag) is idempotent.

sf_ch3_bag_thm

Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.

Fixpoint beq_nat (n m : nat) : bool :=
  match n with
  | O => match m with
         | O => true
         | S m' => false
         end
  | S n' => match m with
            | O => false
            | S m' => beq_nat n' m'
            end
  end.

Inductive natlist : Type :=
  | nil  : natlist
  | cons : nat -> natlist -> natlist.

Notation "x :: l" := (cons x l)
                     (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

Definition bag := natlist.
Definition add (v:nat) (s:bag) : bag 
  := v :: s.

Lemma add_to_empty :
  forall n : nat, add n [] = [n].
Proof.
  induction n as [|n' IHn'].
  reflexivity.
  reflexivity.
Qed.

Lemma beq_id_true :
  forall n : nat, beq_nat n n = true.
Proof.
  induction n as [|n' IHn'].
  - reflexivity.
  - simpl. rewrite <- IHn'. reflexivity.
Qed.

Lemma remove_last :
  forall n : nat, length (remove_one n [n]) = 0.
Proof.
  intros n.
  simpl. rewrite -> beq_id_true. reflexivity.
Qed.

Theorem bag_theorem : 
  forall n : nat, 
  forall b : bag,
  remove_one n (add n b) = b.
Proof.
  intros n b. induction b as [|h t IHb'].
  - simpl. rewrite -> beq_id_true. reflexivity.
  - simpl. rewrite -> beq_id_true. reflexivity.
Qed.