доказав х> = а/\ х <= a -> х =

Question

Как бы один идти о доказательстве следующего

Theorem T: forall x, a: nat, x >= a /\ x <= a -> x = a. 

в Coq?

Answer 1

Если вы не хотите использовать всю мощь omega, я искал бы стандартную библиотеку для антисимметричного свойства <= с использованием SearchPattern или SearchAbout (или Google) и apply le_antisym.

Если вы хотите получить доказательство без использования лемм из библиотеки, перейдите по индукции на x и a.