diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-04-14 19:38:14 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-04-14 20:56:31 -0400 |
| commit | bd962fc6be67c58b88935d924c6183e8f9cbe58b (patch) | |
| tree | 8af6334b5c8be685dd297b8a73a93b8b533c28d0 /src/Curves | |
| parent | 69fc6dabced75fd38eaf89c4186d7de0ccff93b8 (diff) | |
lemmas about ladderstep on zero
Diffstat (limited to 'src/Curves')
| -rw-r--r-- | src/Curves/Montgomery/XZProofs.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/Curves/Montgomery/XZProofs.v b/src/Curves/Montgomery/XZProofs.v index ef708af00..4c42d9464 100644 --- a/src/Curves/Montgomery/XZProofs.v +++ b/src/Curves/Montgomery/XZProofs.v @@ -57,6 +57,21 @@ Module M. | |- _ /\ _ => split end. + Lemma add_0_denominators A B C D + : snd (fst (xzladderstep 0 (pair A 0) (pair C 0))) = 0 + /\ snd (snd (xzladderstep 0 (pair B 0) (pair D 0))) = 0. + Proof. t; fsatz. Qed. + + Lemma add_0_numerator_l A B C D + : snd (fst (xzladderstep 0 (pair 0 C) (pair A 0))) = 0 + /\ snd (snd (xzladderstep 0 (pair 0 D) (pair B 0))) = 0. + Proof. t; fsatz. Qed. + + Lemma add_0_numerator_r A B C D + : snd (fst (xzladderstep 0 (pair C 0) (pair 0 A))) = 0 + /\ snd (snd (xzladderstep 0 (pair D 0) (pair 0 B))) = 0. + Proof. t; fsatz. Qed. + Lemma to_xz_add (x1:F) (Q Q':Mpoint) (difference_correct:match M.coordinates (Madd Q (Mopp Q')) with | ∞ => False (* Q <> Q' *) |