proposition: Lemma split_lshift n m i: @split n m (lshift i) = inl i.
proof: Proof. case split_spec; intros j E. f_equal. apply eq_ord. injection E. congruence. exfalso. injection E. clear E. destruct i as [i Hi]. simpl. intros ->. rewrite leb_plus_r in Hi. discriminate. Qed.
imports: List PeanoNat common comparisons