proposition: Lemma split_spec n m (i: ord (n+m)): split_case i (split i).
proof: Proof. unfold split. case lt_ge_dec; constructor; apply eq_ord; simpl. reflexivity. destruct i as [j Hj]. simpl in *. revert n m e Hj. induction j; destruct n; simpl; auto. discriminate. intros. f_equal. eapply IHj; eassumption. Qed.
imports: List PeanoNat common comparisons