aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil/Tactics.v
blob: 38808e6c783f2ce45015f77a76917d96a54ba192 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
Require Export Crypto.Util.ZUtil.Tactics.CompareToSgn.
Require Export Crypto.Util.ZUtil.Tactics.DivideExistsMul.
Require Export Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
Require Export Crypto.Util.ZUtil.Tactics.LinearSubstitute.
Require Export Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Export Crypto.Util.ZUtil.Tactics.PeelLe.
Require Export Crypto.Util.ZUtil.Tactics.PrimeBound.
Require Export Crypto.Util.ZUtil.Tactics.PullPush.
Require Export Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos.
Require Export Crypto.Util.ZUtil.Tactics.RewriteModSmall.
Require Export Crypto.Util.ZUtil.Tactics.SimplifyFractionsLe.
Require Export Crypto.Util.ZUtil.Tactics.ZeroBounds.
Require Export Crypto.Util.ZUtil.Tactics.Ztestbit.