Make the LeanAuto prover use classical reasoning

This is more straightforwardly compatible with Boogie's semantics and
the use of SMT.

Author: atomb

Source/Provers/LeanAuto/Prelude.lean

@@ -2,7 +2,7 @@ import Auto
 import Auto.Tactic
 import Auto.MathlibEmulator.Basic -- For `Real`
 import Auto.Translation.SMTAttributes
-open Lean Std Auto Auto.SMT.Attribute
+open Lean Std Auto Auto.SMT.Attribute Classical
 
 set_option linter.unusedVariables false
 set_option auto.smt true