fact: Definition split {n m} (i: ord (n+m)): ord n + ord m := match lt_ge_dec i n with | left Hi => inl _ (Ord _ Hi) | right Hj => inr _ (Ord _ (ltb_minus _ _ _ (ord_lt i) Hj)) end.
imports: List PeanoNat common comparisons