fact: Definition composable_pairs_step (n : N) (z : M.t N) : M.t N := let next := triangular_number (N.pred n) in let go i rest := let k j r := let mor := next + i in let dom := triangular_number (j + i) + i in let cod := mor + j in M.add (cod, dom) mor r in N.peano_rect _ rest k (n - i) in N.peano_rect _ z go n.
imports: Coq.NArith.NArith Coq.micromega.Lia Category.Lib Category.Lib.MapDecide Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor