Suppose that we have a simple “compound” proposition, being in fact a conjunction of several other propositions (think, e.g. of being a non-trivial divisor of
n). I can see at least two different methods of formalizing it in Coq. Either we use a direct
Definition or we use an inductive proposition with a single constructor.
Are there “best practices” regarding when to use what definition? Are there any notable differences, except perhaps in formalization style? In my experience, it seems that one tends to require
inversion quite a lot, and the other
unfolding. Otherwise, they are essentially much the same. I have not encountered a good example where I might want to choose one over the other. Is there one?