My understanding (having only used dependent-types -family interactive theorem provers) is that if your property can be expressed in HOL, proving it will require far less human effort to prove than Coq or similar.
A lot of proof automation is based on SAT/SMT solvers like Z3, which are based on classical logic.
"I have been contributing to the development of the Lean Theorem Prover since its inception. I led the development of the first libraries and documentation.."
"Many parts of classical mathematics, however, have not been developed constructively."
https://www.andrew.cmu.edu/user/avigad/research.html
https://www.andrew.cmu.edu/user/avigad/Teaching/classical.pd...