proposition: Lemma composable_pairs_succ n : composable_pairs (N.succ n) = composable_pairs_step (N.succ n) (composable_pairs n).
proof: Proof. unfold composable_pairs. rewrite N.peano_rect_succ; reflexivity. Qed.
imports: Coq.NArith.NArith Coq.micromega.Lia Category.Lib Category.Lib.MapDecide Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Instance.Two Category.Instance.Cat