proposition: Lemma remove_concat A (eq_dec : forall x y : A, {x = y}+{x <> y}) : forall l x, remove eq_dec x (concat l) = flat_map (remove eq_dec x) l.
proof: Proof. intros l x; induction l as [|? ? IHl]; [ reflexivity | simpl ]. rewrite remove_app, IHl; reflexivity. Qed.
imports: PeanoNat