Software Foundations：如何用指定Coq战术证明假前提蕴含式？

你在自学《Software Foundations》时卡在了lower_grade_lowers定理的最后一个子目标，该子目标为：

grade_comparison (Grade F Minus) (Grade F Minus) = Lt ->
grade_comparison (lower_grade (Grade F Minus)) (Grade F Minus) = Lt

其中grade_comparison返回的comparison归纳类型定义为：

Inductive comparison : Set :=
  | Eq : comparison        (* "equal" *)
  | Lt : comparison        (* "less than" *)
  | Gt : comparison.       (* "greater than" *)

按照提示使用lower_grade_F_Minus并简化后，得到命题：

Eq = Lt -> Eq = Lt

你可以用以下两种方法中的任意一种完成证明，均只用到你已掌握的战术：

方法一 #

1. 执行intros H，将前提Eq = Lt引入上下文。
2. 执行rewrite H，把结论中的Eq替换为Lt，此时结论变为Lt = Lt，再执行reflexivity即可完成证明。

方法二 #

1. 执行intros H引入前提。
2. 执行destruct H，由于Eq和Lt是comparison类型的不同构造子，该等式不可能成立，Coq会直接判定此子目标得证。

内容的提问来源于stack exchange，提问作者PeterTN