below is a simple proof in TLAPS of what I believe is your intended result. As Leslie remarked, your difficulties seem to be caused by a confusion between /\ and ^, both of which appear to denote conjunction in your module.
LEMMA ASSUME NEW R \in Nat, \E a \in Nat : R = 2 * a,
NEW N \in Nat, NEW VARIABLE x, x = R * N
PROVE \E y \in Nat : x = 2 * y
Note that it doesn't matter for the validity of this lemma if x is declared as a VARIABLE or CONSTANT.
And no, TLA+ is not primarily designed for reasoning about propositional logic (temporal or otherwise). Have you had a look at the Hyperbook?