Last active
September 20, 2022 00:30
-
-
Save yoshihiro503/c6b64c8cf3f32a5a66601a0e9998b9e0 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
From mathcomp Require Import all_ssreflect. | |
Lemma rensyu : forall i x y, | |
i != 0 -> (x - y) = 0 -> x.+1 - y <= i. | |
Proof. | |
move=> i x y i0 /eqP xy. | |
rewrite -addn1. | |
rewrite leq_subLR. | |
apply: leq_add. | |
by []. | |
by case: i i0. | |
Qed. |
ありがとうございます。i=0の場合は先に考えた方が短くなるんですね。
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
nekoniです。
もう少し簡単にできないかなと思い、やってみました。
i != 0
の仮定がある場合は即case : i =>[|i]//
で大丈夫で、あとはx - y = 0
をそのまま代入できるように変形してみました。