proposition: Lemma split'_decr: forall l1 l2 a b, l1 = a::b::l2 -> length (fst(split' l1)) < length l1 /\ length (snd(split' l1)) < length l1.
proof: Proof. split. + intros; unfold split'; rewrite H. apply Nat.le_lt_trans with (m:=Nat.div2(length (a::b::l2))). rewrite split'_aux_length_fst. apply Nat.le_min_l. simpl; rewrite <- Nat.succ_lt_mono. destruct (length l2); auto. apply Nat.lt_trans with (m:=S n); auto. apply Nat.lt_div2; abstract lia. + intros. rewrite <- (split'_aux_length_preserve l1 l1). assert(0<length (fst (split'_aux l1 l1)) ). { rewrite H. rewrite split'_aux_length_fst. apply Nat.min_glb_lt; simpl; abstract lia. } unfold split'; abstract lia. Qed.
imports: Coq(List Wf_nat Recdef Compare_dec Arith Peano_dec Lia RelationClasses Sorting.Sorted Sorting.Permutation) hydras(DecPreOrder DecPreOrder_Instances Sort_spec)