Я пытаюсь доказать следующую лемму:
lemma
fixes A B C D :: "((real, 3) vec, 3) vec"
and v m :: " (real, 3) vec"
assumes "∃ A. m = D ** A ** B *v v"
shows "∃ A. m = D ** B ** A *v v"
, но я не смог этого сделать, поскольку ∃ A. D ** A**B *v v = D ** B**A *v v можно доказать прямо.Вероятно, из-за ∃ A !.Кто-нибудь может объяснить, почему Изабель / HOL не может доказать это?Спасибо