merging with main

ufmg-smite · Nov 30, 2023 · b367255 · b367255
2 parents 35e0198 + 666dbd8
commit b367255
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/Smt/Reconstruction/Certifying/Arith/MulPosNeg/Tactic.lean b/Smt/Reconstruction/Certifying/Arith/MulPosNeg/Tactic.lean
@@ -133,7 +133,4 @@ def arithMulMeta (va vb vc : Expr) (pos : Bool) (compId : Nat) (thms : List Name
   evalTactic (← `(tactic| exact $(mkIdent fname)))
   trace[smt.profile] m!"[arithMulNeg] end time: {← IO.monoNanosNow}ns"
 
-example {a b c : Real} : 0 > c ∧ a ≤ b → c * a ≥ c * b := by
-  arithMulNeg [a,b,c], 1
-
 end Smt.Reconstruction.Certifying