proposition: Theorem split_list_comm : ∀ α (l la lb : list α), split_list l la lb → split_list l lb la.
proof: Proof. intros A l la lb H. revert la lb H. induction l as [| x]; intros. inversion H; subst; constructor. inversion H; subst; constructor; apply IHl; assumption. Qed.
imports: Utf8 Arith NPeano Sorted Misc