proposition: Lemma lem_split {A} : forall l : list A, 2 <= List.length l -> forall l1 l2, (l1, l2) = ` (split l) -> List.length l1 < List.length l /\ List.length l2 < List.length l.
proof: Proof. sauto. Qed.
imports: Hammer(Tactics) Hammer(Reflect) Arith Lia Sorting.Permutation Program