Yes, symbolic computation, which is what FullSimplify[] carries out, is done in part via equivalence transformations that are programmed into the system. From a purely mathematical viewpoint, one calls these transformations identities or even theorems. One presumes they are based on how the functions are defined and computed in WL (when there exists more than one definition out in the world). Symbolic computation is inescapably based on theory. I don't think there is another way to perform this computation.

In WL, the transformations are often coded as replacement rules. There is a large table of them SimplifyDump`$FSTab[...]. Internally, FullSimplify[] does more or less what @Gianluca Gorni shows:

Block[{Internal`FunctionExpand`$Debug = True},
 FullSimplify[x == q Quotient[x, q] + Mod[x, q]]
 ]

Then exploring which rules cause the transformations, we find these two:

SimplifyDump`$FSTab[540]
Quotient[x, q] /. %
(*
Quotient[SimplifyDump`x_, SimplifyDump`y_] :> 
  Floor[SimplifyDump`x/SimplifyDump`y]
Floor[x/q]
*)

SimplifyDump`$FSTab[680]
Mod[x, q] /. %
(*
Mod[SimplifyDump`x_, SimplifyDump`y_] :> 
  SimplifyDump`x - SimplifyDump`y Floor[SimplifyDump`x/SimplifyDump`y]
x - q Floor[x/q]
*)

I tried that too, but I didn't detect those transformations. How did you find them?

Using Reduce I get the message that it is using FunctionExpand:

Reduce[x == q Quotient[x, q] + Mod[x, q]]

In fact FunctionExpand translates the expression into Floor objects:

FunctionExpand[q Quotient[x, q]]
FunctionExpand[Mod[x, q]]