proposition: Lemma length_remove_not_common : forall l1 l2 acc, length (remove_not_common acc l1 l2) = length acc + length (remove_not_common nil l1 l2).
proof: Proof. fix length_remove_not_common 2. intros l1 l2 acc; case l2; clear l2; simpl. rewrite <- plus_n_O; reflexivity. intros a2 l2; case (mem_bool eq_bool a2 l1). rewrite (length_remove_not_common l1 l2 (a2 :: acc)); rewrite (length_remove_not_common l1 l2 (a2 :: nil)); simpl; apply plus_n_Sm. apply length_remove_not_common. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)