blob: 0f80a75d9796fd2ab2abc3dd540ba159a2b85e17 (
plain)
1
2
3
4
5
6
7
8
9
|
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Util.ZUtil.Definitions.
Local Open Scope Z_scope.
Module Z.
Lemma add_modulo_correct x y modulus :
Z.add_modulo x y modulus = if (modulus <=? x + y) then (x + y) - modulus else (x + y).
Proof. reflexivity. Qed.
End Z.
|
