Towards a Safe and Expressive Automation: Combining Automatic and Interactive Proofs