Constant MATH_AUTO 

pub const MATH_AUTO: &str = r###"-- ============================================
-- AUTO TACTIC: The Infinity Gauntlet
-- ============================================
-- The auto tactic combines ALL decision procedures!
-- It tries each one in sequence until one succeeds:
--   1. True/False (trivial propositions)
--   2. simp  (simplification)
--   3. ring  (polynomial algebra)
--   4. cc    (congruence closure)
--   5. omega (integer arithmetic)
--   6. lia   (linear arithmetic)

-- ============================================
-- SIMPLIFICATION (auto -> simp)
-- ============================================

## Theorem: TrueIsTrue
    Statement: True.
    Proof: auto.

Check TrueIsTrue.

-- ============================================
-- RING ALGEBRA (auto -> ring)
-- ============================================

## Theorem: AddCommutative
    Statement: (Eq (add a b) (add b a)).
    Proof: auto.

Check AddCommutative.

## Theorem: AddAssociative
    Statement: (Eq (add (add a b) c) (add a (add b c))).
    Proof: auto.

Check AddAssociative.

## Theorem: MulDistributes
    Statement: (Eq (mul a (add b c)) (add (mul a b) (mul a c))).
    Proof: auto.

Check MulDistributes.

-- ============================================
-- CONGRUENCE CLOSURE (auto -> cc)
-- ============================================

## Theorem: FunctionReflexive
    Statement: (Eq (f x) (f x)).
    Proof: auto.

Check FunctionReflexive.

-- ============================================
-- INTEGER ARITHMETIC (auto -> omega)
-- ============================================

## Theorem: TwoLessThanFive
    Statement: (Lt 2 5).
    Proof: auto.

Check TwoLessThanFive.

## Theorem: StrictToNonStrict
    Statement: (implies (Gt x 0) (Ge x 1)).
    Proof: auto.

Check StrictToNonStrict.

## Theorem: XLessThanSucc
    Statement: (Lt x (add x 1)).
    Proof: auto.

Check XLessThanSucc.

-- ============================================
-- LINEAR ARITHMETIC (auto -> lia/omega)
-- ============================================

## Theorem: LeReflexive
    Statement: (Le x x).
    Proof: auto.

Check LeReflexive.

## Theorem: LeTransitive
    Statement: (implies (Le x y) (implies (Le y z) (Le x z))).
    Proof: auto.

Check LeTransitive.

-- ============================================
-- THE POWER OF AUTO
-- ============================================
-- With auto, you don't need to think about
-- which tactic to use. Just say:
--
--     Proof: auto.
--
-- And the system figures it out!
--
-- auto combines ALL five stones:
-- - ring: polynomial equalities
-- - lia: linear rational arithmetic
-- - cc: congruence closure
-- - simp: simplification
-- - omega: true integer arithmetic
--
-- This is the Infinity Gauntlet of tactics!
"###;