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. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
ありがとうございます。i=0の場合は先に考えた方が短くなるんですね。