[Abhinav2000]

Thanks Kevin. It seems like having both approaches is more flexible and thus more general (which can hopefully only be a good thing?). One could always replace a proof by contradiction later with a direct proof, but there's definitely value in using it in the meantime (at least in my uneducated view).

p.s. could you let me know your e-mail so I can keep for future reference, as I'm also working on a hobby project for automated theorem solving.