proposition: Lemma without_red_remove_not_common : forall l1 l2, without_red l1 -> without_red l2 -> without_red (remove_not_common nil l1 l2).
proof: Proof. intros l1 l2 wr1 wr2; apply without_red_remove_not_common_aux; trivial. intros e [ H _ ]; contradiction. simpl; trivial. Qed.
imports: List more_list list_permut Arith