I'm working through Software Foundations on my own and am stuck on the final bullet for lower_grade_lowers. My theorem follows the hint pretty well until that final case which is obviously the crux of the problem but I'm not posting the example as it's used for homework assignments. My problem is the case with the sub-goal:
grade_comparison (Grade F Minus) (Grade F Minus) = Lt ->
grade_comparison (lower_grade (Grade F Minus)) (Grade F Minus) = Lt
grade_comparison is a definition that returns the inductive
Inductive comparison : Set :=
| Eq : comparison (* "equal" *)
| Lt : comparison (* "less than" *)
| Gt : comparison. (* "greater than" *)
Using lower_grade_F_Minus as suggested in the help comments and then simplifying, I get a proposition which seems like it should be easy to prove. Either
grade_comparison (Grade F Minus) (Grade F Minus) = Lt ->
grade_comparison (Grade F Minus) (Grade F Minus) = Lt
or simplified
Eq = Lt -> Eq = Lt
Given the premise of the conditional is always false, it seems trivial to prove this statement, but from searching online for how to actually write this out in tactics, it sounds like this can only be covered by intuitionistic propositional calculus which hasn't been covered at this point in the text so it seems like my approach is getting ahead of the text and I missed something.
Is there a simpler way to show that a proposition with a false premise is always true using only intros, destruct, simpl, rewrite and reflexivity which were the only tactics covered so far?
Naturally as soon as I post this question, I reread prior examples and was overthinking the problem. A simple rewrite using the hypothesis is all that's needed to turn the implication into a trivial equality and the grader accepts the solution.