proposition: Lemma r_pow_succ_equiv: forall n r1 r2, r1 <==> r2 -> r_pow r1 n <==> r_pow r2 n -> r_pow r1 (S n) <==> r_pow r2 (S n).
proof: Proof. unfold REquiv; intros. repeat rewrite r_pow_rw in *. apply pow_succ_equiv; auto. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang