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. intro l1; functional induction (split l1). - discriminate. - discriminate. - injection 1; intros; subst. rewrite e0 in IHp; simpl in IHp; simpl. destruct l3. inversion e0; abstract lia. destruct l3; [inversion e0; simpl; lia|]. specialize (IHp l3 a a1 (eq_refl _)); 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)