proposition: Theorem partition_inv_nil (l : list A): partition l = ([], []) <-> l = [].
proof: Proof. split. - destruct l as [|a l']. * intuition. * simpl. destruct (f a), (partition l'); now intros [= -> ->]. - now intros ->. Qed.
imports: PeanoNat