proposition: Lemma split_rshift n m i: @split n m (rshift i) = inr i.
proof: Proof. case split_spec; intros j E. exfalso. injection E. clear E. destruct j as [j Hj]. simpl. intros <-. rewrite leb_plus_r in Hj. discriminate. f_equal. apply eq_ord. symmetry. injection E. apply Nat.add_cancel_l. Qed.
imports: List PeanoNat common comparisons