proposition: Theorem rm_not_in: forall (a: A) l1 l2, olist l1 -> olist l2 -> In a l1 -> ~ In a (rm l1 l2).
proof: Proof. intros a l1; generalize a; elim l1; simpl; auto; clear a l1. intros b l1 Rec a l2 H1 H2. assert (O1: olist l1); try apply olist_inv with (1 := H1). intros [H | H]; subst; auto. generalize H2; elim l2; simpl; auto with datatypes; clear l2 H2. intros b l2 Rec1 H2. assert (O2: olist l2); try apply olist_inv with (1 := H2). case_eq (weight a b); auto with datatypes; intros H3. intros H4; absurd (In a (b :: l2)); auto. simpl; intros [H5 | H5]; subst. rewrite weight_refl in H3; discriminate. rewrite weight_anti_sym in H3; rewrite (olist_weight b a l2) in H3; try discriminate; auto. apply (rm_incl l1 (b :: l2) a); auto. assert (a = b); subst. apply weight_exact with (1 := H3). intros H4; absurd (In b l2); auto. assert (H5: ulist (b :: l2)); try apply olist_ulist; auto. inversion H5; auto. apply (rm_incl l1 l2 b); auto. simpl; intros [H4 | H4]; subst. rewrite weight_refl in H3; discriminate. case Rec1; auto. generalize H2; elim l2; simpl; auto with datatypes; clear l2 H2. intros c l2 Rec1 H2. assert (O2: olist l2); try apply olist_inv with (1 := H2). case_eq (weight b c); auto with datatypes; intros H3. simpl; intros [H4 | H4]; subst. rewrite (olist_weight b a l1) in H3; auto; discriminate. case Rec1; auto. Qed.
imports: List Permutation UList