proposition: Lemma split_length : forall x l, let (l1,l2) := split l x in List.length l1 + List.length l2 = List.length l.
proof: Proof. clear. intros x l. functional induction (split l x). reflexivity. simpl. rewrite e0 in IHp. lia. simpl;rewrite e0 in IHp. lia. Qed.
imports: CoLoR(more_list decidable_set list_set) Coq(List Lia FunInd)