proposition: Lemma included_remove_red : forall e l, In e (remove_red l) -> In e l.
proof: Proof. intros x l; induction l as [ | e le ]. contradiction. simpl; destruct (In_dec eq_elt_dec e le) as [ _ | _]. intro; right; apply IHle; trivial. intros [x_eq_e | x_in_rrle]; simpl. left; trivial. right; apply IHle; trivial. Qed.
imports: List more_list list_permut Arith