diff options
Diffstat (limited to 'src/Util/ZUtil/Div/Bootstrap.v')
| -rw-r--r-- | src/Util/ZUtil/Div/Bootstrap.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Div/Bootstrap.v b/src/Util/ZUtil/Div/Bootstrap.v new file mode 100644 index 000000000..3b9338073 --- /dev/null +++ b/src/Util/ZUtil/Div/Bootstrap.v @@ -0,0 +1,12 @@ +(** Basic lemmas about [Z.div] for bootstrapping various tactics *) +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Local Open Scope Z_scope. + +Module Z. + Lemma div_0_r_eq a b : b = 0 -> a / b = 0. + Proof. intro; subst; auto with zarith. Qed. + Hint Resolve div_0_r_eq : zarith. + Hint Rewrite div_0_r_eq using assumption : zsimplify. +End Z. |