forked from mit-plv/fiat-crypto
-
Notifications
You must be signed in to change notification settings - Fork 1
/
ZUtil.v
73 lines (73 loc) · 2.8 KB
/
ZUtil.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
Require Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv.
Require Coq.micromega.Lia Coq.Arith.Arith.
Require Crypto.Util.ZUtil.AddGetCarry.
Require Crypto.Util.ZUtil.AddModulo.
Require Crypto.Util.ZUtil.CC.
Require Crypto.Util.ZUtil.CPS.
Require Crypto.Util.ZUtil.Definitions.
Require Crypto.Util.ZUtil.DistrIf.
Require Crypto.Util.ZUtil.Div.
Require Crypto.Util.ZUtil.Div.Bootstrap.
Require Crypto.Util.ZUtil.Divide.
Require Crypto.Util.ZUtil.Divide.Bool.
Require Crypto.Util.ZUtil.EquivModulo.
Require Crypto.Util.ZUtil.Ge.
Require Crypto.Util.ZUtil.Hints.
Require Crypto.Util.ZUtil.Hints.Core.
Require Crypto.Util.ZUtil.Hints.PullPush.
Require Crypto.Util.ZUtil.Hints.ZArith.
Require Crypto.Util.ZUtil.Hints.Ztestbit.
Require Crypto.Util.ZUtil.Land.
Require Crypto.Util.ZUtil.Land.Fold.
Require Crypto.Util.ZUtil.LandLorBounds.
Require Crypto.Util.ZUtil.LandLorShiftBounds.
Require Crypto.Util.ZUtil.Lor.
Require Crypto.Util.ZUtil.Le.
Require Crypto.Util.ZUtil.Lnot.
Require Crypto.Util.ZUtil.Log2.
Require Crypto.Util.ZUtil.ModInv.
Require Crypto.Util.ZUtil.Modulo.
Require Crypto.Util.ZUtil.Modulo.Bootstrap.
Require Crypto.Util.ZUtil.Modulo.PullPush.
Require Crypto.Util.ZUtil.Morphisms.
Require Crypto.Util.ZUtil.Mul.
Require Crypto.Util.ZUtil.MulSplit.
Require Crypto.Util.ZUtil.N2Z.
Require Crypto.Util.ZUtil.Notations.
Require Crypto.Util.ZUtil.Odd.
Require Crypto.Util.ZUtil.Ones.
Require Crypto.Util.ZUtil.Opp.
Require Crypto.Util.ZUtil.Peano.
Require Crypto.Util.ZUtil.Pow.
Require Crypto.Util.ZUtil.Pow2.
Require Crypto.Util.ZUtil.Pow2Mod.
Require Crypto.Util.ZUtil.Quot.
Require Crypto.Util.ZUtil.Rshi.
Require Crypto.Util.ZUtil.Sgn.
Require Crypto.Util.ZUtil.Shift.
Require Crypto.Util.ZUtil.Sorting.
Require Crypto.Util.ZUtil.Stabilization.
Require Crypto.Util.ZUtil.Tactics.
Require Crypto.Util.ZUtil.Tactics.CompareToSgn.
Require Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
Require Crypto.Util.ZUtil.Tactics.DivideExistsMul.
Require Crypto.Util.ZUtil.Tactics.LinearSubstitute.
Require Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Crypto.Util.ZUtil.Tactics.PeelLe.
Require Crypto.Util.ZUtil.Tactics.PrimeBound.
Require Crypto.Util.ZUtil.Tactics.PullPush.
Require Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
Require Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos.
Require Crypto.Util.ZUtil.Tactics.RewriteModSmall.
Require Crypto.Util.ZUtil.Tactics.RewriteModDivide.
Require Crypto.Util.ZUtil.Tactics.SimplifyFractionsLe.
Require Crypto.Util.ZUtil.Tactics.SplitMinMax.
Require Crypto.Util.ZUtil.Tactics.ZeroBounds.
Require Crypto.Util.ZUtil.Tactics.Ztestbit.
Require Crypto.Util.ZUtil.Testbit.
Require Crypto.Util.ZUtil.Z2Nat.
Require Crypto.Util.ZUtil.ZSimplify.
Require Crypto.Util.ZUtil.ZSimplify.Autogenerated.
Require Crypto.Util.ZUtil.ZSimplify.Core.
Require Crypto.Util.ZUtil.ZSimplify.Simple.
Require Crypto.Util.ZUtil.Zselect.