proposition: Theorem elements_in_partition l l1 l2: partition l = (l1, l2) -> forall x:A, In x l <-> In x l1 \/ In x l2.
proof: Proof. revert l1 l2. induction l as [| a l' Hrec]; simpl; intros l1 l2 Eq x. - injection Eq as [= <- <-]. tauto. - destruct (partition l') as (left, right). specialize (Hrec left right eq_refl x). destruct (f a); injection Eq as [= <- <-]; simpl; tauto. Qed.
imports: PeanoNat