fact: Definition tetrahedral_number (n : N) := (n * (n + 1) * (n + 2)) / 6.
imports: Coq.NArith.NArith Coq.micromega.Lia Category.Lib Category.Lib.MapDecide Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor