Basic theorem proving in Mathematica?

Mathematica does have such a thing, though it's unfortunately not as trivial as one would hope, as that:

FindEquationalProof cannot prove theorems involving arithmetic operators by default

As such, an example:

FindEquationalProof[a == b c, {a/c == b, c == 1}]

Failure["PropositionFalse", 
Association["MessageTemplate" -> TemplateObject[{
"The proposition could not be reduced to True."}

If you read the docs under possible issues a solution to work around it.

FindEquationalProof[ForAll[x, f[4*x] == 4*f[x]], {ForAll[x, f[2*x] == 2*f[x]]}]
(*Same error as above*)

FindEquationalProof[ForAll[a, f[mult[4, x]] == mult[4, f[x]]], {ForAll[x, f[mult[2, x]] == mult[2, f[x]]], ForAll[{x, y, z}, mult[x, mult[y, z]] == mult[mult[x, y], z]], mult[2, 2] == 4}]

As such one would have to build in the logic of multiplying for your theorem to be found.

This is something of a draft since I would have preferred to avoid writing the axioms for equality. But this seems blocked, since the documentation says "The statements stmt can consist of arbitrary logical combinations of predicates" where predicates don't seem to include == (equality). Comments and corrections welcome.

equalityAxioms = 
 {ForAll[{x}, eq[x, x]],
  ForAll[{x, y}, Implies[eq[x, y], eq[y, x]]],
  ForAll[{x, y, z}, Implies[And[eq[x, y], eq[y, z]], eq[x, z]]]}
multiplicationAxioms = 
 {ForAll[{a, b}, eq[m[a, b], m[b, a]]],
  ForAll[{a, b, c}, eq[m[a, m[b, c]], m[m[a, b], c]]],
  ForAll[{a}, eq[m[a, 1], a]]}
primalityAxiom = {Implies[prime[x], 
   ForAll[{a, b, x}, 
    Implies[eq[x, 
      m[a, b]], (eq[a, x] && eq[b, 1]) || (eq[a, 1] && eq[b, x])]]]}
FindEquationalProof[(eq[p, n]), 
 Union[equalityAxioms, 
  primalityAxiom, {prime[p], ! (eq[n, 1]), eq[p, m[n, q]]}]]