Assume that the statement we want to prove has a proof.
Can we find it with only the “standard” Coq tactics?
i.e. is programming a custom tactic ever necessary? (not sufficient is not what I care, if it has a proof this in theory could be a silly tactic that encodes the proof of the statement which is not interested)
Motivation: I recently learned that one can implement their own tactics…!