输入格式

一行一个字符串。

输出格式

一行一个长度不超过 100 的字符串。

若有多个答案满足条件，你可输出任意合法的答案。

样例输入1

n = n

样例输出1

rfl

样例输入2

n + 0 = n

样例输出2

rw [Nat.add_zero]

样例 2 解释

apply Nat.add_zero 也是正确答案

数据范围与约定

保证唯一的测试点输入为

\exists (p q : Nat), Prime p \and Prime q \and 2 * n + 4 = p + q

提示

The proof is simple in Unknown Language.