Как использовать «поле» с рациональными числами?

Question

Кто-нибудь может мне сказать, почему тактика "поле" не работает, когда я пытаюсь доказать следующую цель с использованием рациональных чисел?

nat_to_Q 3 * nat_to_Q n * nat_to_Q n + nat_to_Q 3 * nat_to_Q n +
nat_to_Q 3 * nat_to_Q n + nat_to_Q 3 + nat_to_Q 3 * nat_to_Q n + 
nat_to_Q 3 + nat_to_Q n * nat_to_Q n * nat_to_Q n + nat_to_Q n * nat_to_Q n +
nat_to_Q n * nat_to_Q n * nat_to_Q 2 + nat_to_Q n * nat_to_Q 2 ==
nat_to_Q 3 * nat_to_Q n * nat_to_Q n * nat_to_Q n +
nat_to_Q 6 * nat_to_Q n * nat_to_Q n + nat_to_Q 11 * nat_to_Q n + 
nat_to_Q 6

Примечание: n - это nat, а nat_to_Q - (Z.of_nat n # Pos.of_nat 1).

Большое спасибо, Marcus.

Answer 1

Давайте уберем принуждения, чтобы их было легче читать:

3 * n * n + 3 * n +
    3 * n + 3 * n +
        3 + n * n * n + n * n +
n * n * 2 + n * 2 ==
3 * n * n * n + 
6 * n * n + 11 * n + 6

Теперь мы можем видеть проблему: цель не держится. Коэффициент 3-го порядка в левой части равен 1, но в правой части он равен 3.