fact: Definition composable_pairs : N → M.t N := N.peano_rect _ (M.empty _) (λ n, composable_pairs_step (N.succ n)).
imports: Coq.NArith.NArith Coq.micromega.Lia Category.Lib Category.Lib.MapDecide Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor