proposition: Lemma split_ordS m i: @split 1 m (ordS i) = inr i.
proof: Proof. case split_spec; intros j Hj. rewrite (ord0_unique j) in Hj. discriminate. destruct i; destruct j. injection Hj. intros <-. f_equal. now apply eq_ord. Qed.
imports: List PeanoNat common comparisons