Merge of fixedlength and master

9 files changed, 1629 insertions, 836 deletions

diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v
new file mode 100644
index 000000000..ca1394115
--- /dev/null
+++ b/src/Util/AdditionChainExponentiation.v
@@ -0,0 +1,102 @@
+Require Import Coq.Lists.List Coq.Lists.SetoidList. Import ListNotations.
+Require Import Crypto.Util.ListUtil.
+Require Import Algebra. Import Monoid ScalarMult.
+Require Import VerdiTactics.
+Require Import Crypto.Util.Option.
+
+Section AddChainExp.
+  Function add_chain (is:list (nat*nat)) : list nat :=
+    match is with
+    | nil => nil
+    | (i,j)::is' =>
+      let chain' := add_chain is' in
+      nth_default 1 chain' i + nth_default 1 chain' j::chain'
+    end.
+
+Example wikipedia_addition_chain : add_chain (rev [
+(0, 0); (* 2 = 1 + 1 *) (* the indices say how far back the chain to look *)
+(0, 1); (* 3 = 2 + 1 *)
+(0, 0); (* 6 = 3 + 3 *)
+(0, 0); (* 12 = 6 + 6 *)
+(0, 0); (* 24 = 12 + 12 *)
+(0, 2); (* 30 = 24 + 6 *)
+(0, 6)] (* 31 = 30 + 1 *)
+) = [31; 30; 24; 12; 6; 3; 2]. reflexivity. Qed.
+
+  Context {G eq op id} {monoid:@Algebra.monoid G eq op id}.
+  Local Infix "=" := eq : type_scope.
+
+  Function add_chain_exp (is : list (nat*nat)) (x : G) : list G :=
+    match is with
+    | nil => nil
+    | (i,j)::is' =>
+      let chain' := add_chain_exp is' x in
+      op (nth_default x chain' i) (nth_default x chain' j) ::chain'
+    end.
+
+  Fixpoint scalarmult n (x : G) : G := match n with
+    | O    => id
+    | S n' => op x (scalarmult n' x)
+    end.
+
+  Lemma add_chain_exp_step : forall i j is x,
+    (forall n, nth_default x (add_chain_exp is x) n = scalarmult (nth_default 1 (add_chain is) n) x) ->
+    (eqlistA eq)
+    (add_chain_exp ((i,j) :: is) x)
+      (op (scalarmult (nth_default 1 (add_chain is) i) x)
+         (scalarmult (nth_default 1 (add_chain is) j) x) :: add_chain_exp is x).
+  Proof.
+    intros.
+    unfold add_chain_exp; fold add_chain_exp.
+    apply eqlistA_cons; [ | reflexivity].
+    f_equiv; auto.
+  Qed.
+
+  Lemma scalarmult_same : forall c x y, eq x y -> eq (scalarmult c x) (scalarmult c y).
+  Proof.
+    induction c; intros.
+    + reflexivity.
+    + simpl. f_equiv; auto.
+  Qed.
+
+  Lemma scalarmult_pow_add : forall a b x, scalarmult (a + b) x = op (scalarmult a x) (scalarmult b x).
+  Proof.
+    intros; eapply scalarmult_add_l.
+    Grab Existential Variables.
+    2:eauto.
+    econstructor; try reflexivity.
+    repeat intro; subst.
+    auto using scalarmult_same.
+  Qed.
+
+  Lemma add_chain_exp_spec : forall is x,
+    (forall n, nth_default x (add_chain_exp is x) n = scalarmult (nth_default 1 (add_chain is) n) x).
+  Proof.
+    induction is; intros.
+    + simpl; rewrite !nth_default_nil. cbv.
+      symmetry; apply right_identity.
+    + destruct a.
+      rewrite add_chain_exp_step by auto.
+      unfold add_chain; fold add_chain.
+      destruct n.
+      - rewrite !nth_default_cons, scalarmult_pow_add. reflexivity.
+      - rewrite !nth_default_cons_S; auto.
+  Qed.
+
+  Lemma add_chain_exp_answer : forall is x n, Logic.eq (head (add_chain is)) (Some n) ->
+    option_eq eq (Some (scalarmult n x)) (head (add_chain_exp is x)).
+  Proof.
+    intros.
+    change head with (fun {T} (xs : list T) => nth_error xs 0) in *.
+    cbv beta in *.
+    cbv [option_eq].
+    destruct is; [ discriminate | ].
+    destruct p.
+    simpl in *.
+    injection H; clear H; intro H.
+    subst n.
+    rewrite !add_chain_exp_spec.
+    apply scalarmult_pow_add.
+  Qed.
+
+End AddChainExp.
\ No newline at end of file
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 0426c0834..169564c23 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -1,22 +1,112 @@
 Require Import Coq.Lists.List.
 Require Import Coq.omega.Omega.
 Require Import Coq.Arith.Peano_dec.
+Require Import Coq.Classes.Morphisms.
 Require Import Crypto.Tactics.VerdiTactics.
+Require Import Coq.Numbers.Natural.Peano.NPeano.
+Require Import Crypto.Util.NatUtil.
+
+Create HintDb distr_length discriminated.
+Create HintDb simpl_set_nth discriminated.
+Create HintDb simpl_update_nth discriminated.
+Create HintDb simpl_nth_default discriminated.
+Create HintDb simpl_nth_error discriminated.
+Create HintDb simpl_firstn discriminated.
+Create HintDb simpl_skipn discriminated.
+Create HintDb simpl_fold_right discriminated.
+Create HintDb simpl_sum_firstn discriminated.
+Create HintDb pull_nth_error discriminated.
+Create HintDb push_nth_error discriminated.
+Create HintDb pull_nth_default discriminated.
+Create HintDb push_nth_default discriminated.
+Create HintDb pull_firstn discriminated.
+Create HintDb push_firstn discriminated.
+Create HintDb pull_update_nth discriminated.
+Create HintDb push_update_nth discriminated.
+
+Hint Rewrite
+  @app_length
+  @rev_length
+  @map_length
+  @seq_length
+  @fold_left_length
+  @split_length_l
+  @split_length_r
+  @firstn_length
+  @combine_length
+  @prod_length
+  : distr_length.
+
+Definition sum_firstn l n := fold_right Z.add 0%Z (firstn n l).
+
+Fixpoint map2 {A B C} (f : A -> B -> C) (la : list A) (lb : list B) : list C :=
+  match la with
+  | nil => nil
+  | a :: la' => match lb with
+                | nil => nil
+                | b :: lb' => f a b :: map2 f la' lb'
+                end
+  end.
+
+(* xs[n] := f xs[n] *)
+Fixpoint update_nth {T} n f (xs:list T) {struct n} :=
+	match n with
+	| O => match xs with
+				 | nil => nil
+				 | x'::xs' => f x'::xs'
+				 end
+	| S n' =>  match xs with
+				 | nil => nil
+				 | x'::xs' => x'::update_nth n' f xs'
+				 end
+  end.
+
+(* xs[n] := x *)
+Definition set_nth {T} n x (xs:list T)
+  := update_nth n (fun _ => x) xs.
+
+Definition splice_nth {T} n (x:T) xs := firstn n xs ++ x :: skipn (S n) xs.
+Hint Unfold splice_nth.
 
 Ltac boring :=
   simpl; intuition;
   repeat match goal with
            | [ H : _ |- _ ] => rewrite H; clear H
            | _ => progress autounfold in *
-           | _ => progress try autorewrite with core
+           | _ => progress autorewrite with core
            | _ => progress simpl in *
            | _ => progress intuition
          end; eauto.
 
+Ltac boring_list :=
+  repeat match goal with
+         | _ => progress boring
+         | _ => progress autorewrite with distr_length simpl_nth_default simpl_update_nth simpl_set_nth simpl_nth_error in *
+         end.
+
+Lemma nth_default_cons : forall {T} (x u0 : T) us, nth_default x (u0 :: us) 0 = u0.
+Proof. auto. Qed.
+
+Hint Rewrite @nth_default_cons : simpl_nth_default.
+Hint Rewrite @nth_default_cons : push_nth_default.
+
+Lemma nth_default_cons_S : forall {A} us (u0 : A) n d,
+  nth_default d (u0 :: us) (S n) = nth_default d us n.
+Proof. boring. Qed.
+
+Hint Rewrite @nth_default_cons_S : simpl_nth_default.
+Hint Rewrite @nth_default_cons_S : push_nth_default.
+
+Lemma nth_default_nil : forall {T} n (d : T), nth_default d nil n = d.
+Proof. induction n; boring. Qed.
+
+Hint Rewrite @nth_default_nil : simpl_nth_default.
+Hint Rewrite @nth_default_nil : push_nth_default.
+
 Lemma nth_error_nil_error : forall {A} n, nth_error (@nil A) n = None.
-Proof.
-intros. induction n; boring.
-Qed.
+Proof. induction n; boring. Qed.
+
+Hint Rewrite @nth_error_nil_error : simpl_nth_error.
 
 Ltac nth_tac' :=
   intros; simpl in *; unfold error,value in *; repeat progress (match goal with
@@ -69,6 +159,7 @@ Proof.
   induction i; destruct xs; nth_tac'; rewrite IHi by omega; auto.
 Qed.
 Hint Resolve nth_error_length_error.
+Hint Rewrite @nth_error_length_error using omega : simpl_nth_error.
 
 Lemma map_nth_default : forall (A B : Type) (f : A -> B) n x y l,
   (n < length l) -> nth_default y (map f l) n = f (nth_default x l n).
@@ -82,6 +173,8 @@ Proof.
   omega.
 Qed.
 
+Hint Rewrite @map_nth_default using omega : push_nth_default.
+
 Ltac nth_tac :=
   repeat progress (try nth_tac'; try (match goal with
     | [ H: nth_error (map _ _) _ = Some _ |- _ ] => destruct (nth_error_map _ _ _ _ _ _ H); clear H
@@ -90,46 +183,139 @@ Ltac nth_tac :=
   end)).
 
 Lemma app_cons_app_app : forall T xs (y:T) ys, xs ++ y :: ys = (xs ++ (y::nil)) ++ ys.
+Proof. induction xs; boring. Qed.
+
+Lemma unfold_set_nth {T} n x
+  : forall xs,
+    @set_nth T n x xs
+    = match n with
+      | O => match xs with
+	     | nil => nil
+	     | x'::xs' => x::xs'
+	     end
+      | S n' =>  match xs with
+		 | nil => nil
+		 | x'::xs' => x'::set_nth n' x xs'
+		 end
+      end.
 Proof.
-	induction xs; boring.
+  induction n; destruct xs; reflexivity.
 Qed.
 
-(* xs[n] := x *)
-Fixpoint set_nth {T} n x (xs:list T) {struct n} :=
-	match n with
-	| O => match xs with
-				 | nil => nil
-				 | x'::xs' => x::xs'
-				 end
-	| S n' =>  match xs with
-				 | nil => nil
-				 | x'::xs' => x'::set_nth n' x xs'
-				 end
-  end.
+Lemma simpl_set_nth_0 {T} x
+  : forall xs,
+    @set_nth T 0 x xs
+    = match xs with
+      | nil => nil
+      | x'::xs' => x::xs'
+      end.
+Proof. intro; rewrite unfold_set_nth; reflexivity. Qed.
 
-Lemma nth_set_nth : forall m {T} (xs:list T) (n:nat) (x x':T),
-  nth_error (set_nth m x xs) n =
+Lemma simpl_set_nth_S {T} x n
+  : forall xs,
+    @set_nth T (S n) x xs
+    = match xs with
+      | nil => nil
+      | x'::xs' => x'::set_nth n x xs'
+      end.
+Proof. intro; rewrite unfold_set_nth; reflexivity. Qed.
+
+Hint Rewrite @simpl_set_nth_S @simpl_set_nth_0 : simpl_set_nth.
+
+Lemma update_nth_ext {T} f g n
+  : forall xs, (forall x, nth_error xs n = Some x -> f x = g x)
+               -> @update_nth T n f xs = @update_nth T n g xs.
+Proof.
+  induction n; destruct xs; simpl; intros H;
+    try rewrite IHn; try rewrite H;
+      try congruence; trivial.
+Qed.
+
+Global Instance update_nth_Proper {T}
+  : Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@update_nth T).
+Proof. repeat intro; subst; apply update_nth_ext; trivial. Qed.
+
+Lemma update_nth_id_eq_specific {T} f n
+  : forall (xs : list T) (H : forall x, nth_error xs n = Some x -> f x = x),
+    update_nth n f xs = xs.
+Proof.
+  induction n; destruct xs; simpl; intros;
+    try rewrite IHn; try rewrite H; unfold value in *;
+      try congruence; assumption.
+Qed.
+
+Hint Rewrite @update_nth_id_eq_specific using congruence : simpl_update_nth.
+
+Lemma update_nth_id_eq : forall {T} f (H : forall x, f x = x) n (xs : list T),
+    update_nth n f xs = xs.
+Proof. intros; apply update_nth_id_eq_specific; trivial. Qed.
+
+Hint Rewrite @update_nth_id_eq using congruence : simpl_update_nth.
+
+Lemma update_nth_id : forall {T} n (xs : list T),
+    update_nth n (fun x => x) xs = xs.
+Proof. intros; apply update_nth_id_eq; trivial. Qed.
+
+Hint Rewrite @update_nth_id : simpl_update_nth.
+
+Lemma nth_update_nth : forall m {T} (xs:list T) (n:nat) (f:T -> T),
+  nth_error (update_nth m f xs) n =
   if eq_nat_dec n m
-  then (if lt_dec n (length xs) then Some x else None)
+  then option_map f (nth_error xs n)
   else nth_error xs n.
 Proof.
-	induction m.
+  induction m.
+  { destruct n, xs; auto. }
+  { destruct xs, n; intros; simpl; auto;
+      [ | rewrite IHm ]; clear IHm;
+        edestruct eq_nat_dec; reflexivity. }
+Qed.
 
-	destruct n, xs; auto.
+Hint Rewrite @nth_update_nth : push_nth_error.
+Hint Rewrite <- @nth_update_nth : pull_nth_error.
 
-	intros; destruct xs, n; auto.
-	simpl; unfold error; match goal with
-		[ |- None = if ?x then None else None ] => destruct x
-	end; auto.
+Lemma length_update_nth : forall {T} i f (xs:list T), length (update_nth i f xs) = length xs.
+Proof.
+  induction i, xs; boring.
+Qed.
 
-	simpl nth_error; erewrite IHm by auto; clear IHm.
-	destruct (eq_nat_dec n m), (eq_nat_dec (S n) (S m)); nth_tac.
+Hint Rewrite @length_update_nth : distr_length.
+
+(** TODO: this is in the stdlib in 8.5; remove this when we move to 8.5-only *)
+Lemma nth_error_None : forall (A : Type) (l : list A) (n : nat), nth_error l n = None <-> length l <= n.
+Proof.
+  intros A l n.
+  destruct (le_lt_dec (length l) n) as [H|H];
+    split; intro H';
+      try omega;
+      try (apply nth_error_length_error in H; tauto);
+      try (apply nth_error_error_length in H'; omega).
 Qed.
 
-Lemma length_set_nth : forall {T} i (x:T) xs, length (set_nth i x xs) = length xs.
-  induction i, xs; boring.
+(** TODO: this is in the stdlib in 8.5; remove this when we move to 8.5-only *)
+Lemma nth_error_Some : forall (A : Type) (l : list A) (n : nat), nth_error l n <> None <-> n < length l.
+Proof. intros; rewrite nth_error_None; split; omega. Qed.
+
+Lemma nth_set_nth : forall m {T} (xs:list T) (n:nat) x,
+  nth_error (set_nth m x xs) n =
+  if eq_nat_dec n m
+  then (if lt_dec n (length xs) then Some x else None)
+  else nth_error xs n.
+Proof.
+  intros; unfold set_nth; rewrite nth_update_nth.
+  destruct (nth_error xs n) eqn:?, (lt_dec n (length xs)) as [p|p];
+    rewrite <- nth_error_Some in p;
+    solve [ reflexivity
+          | exfalso; apply p; congruence ].
 Qed.
 
+Hint Rewrite @nth_set_nth : push_nth_error.
+
+Lemma length_set_nth : forall {T} i x (xs:list T), length (set_nth i x xs) = length xs.
+Proof. intros; apply length_update_nth. Qed.
+
+Hint Rewrite @length_set_nth : distr_length.
+
 Lemma nth_error_length_exists_value : forall {A} (i : nat) (xs : list A),
   (i < length xs)%nat -> exists x, nth_error xs i = Some x.
 Proof.
@@ -143,52 +329,88 @@ Proof.
   destruct (nth_error_length_exists_value i xs); intuition; congruence.
 Qed.
 
-Lemma nth_error_value_eq_nth_default : forall {T} i xs (x d:T),
+Lemma nth_error_value_eq_nth_default : forall {T} i (x : T) xs,
   nth_error xs i = Some x -> forall d, nth_default d xs i = x.
 Proof.
   unfold nth_default; boring.
 Qed.
 
+Hint Rewrite @nth_error_value_eq_nth_default using eassumption : simpl_nth_default.
+
 Lemma skipn0 : forall {T} (xs:list T), skipn 0 xs = xs.
+Proof. auto. Qed.
+
+Lemma firstn0 : forall {T} (xs:list T), firstn 0 xs = nil.
+Proof. auto. Qed.
+
+Lemma splice_nth_equiv_update_nth : forall {T} n f d (xs:list T),
+  splice_nth n (f (nth_default d xs n)) xs =
+  if lt_dec n (length xs)
+  then update_nth n f xs
+  else xs ++ (f d)::nil.
 Proof.
-  auto.
+  induction n, xs; boring_list.
+  do 2 break_if; auto; omega.
 Qed.
 
-Lemma firstn0 : forall {T} (xs:list T), firstn 0 xs = nil.
+Lemma splice_nth_equiv_update_nth_update : forall {T} n f d (xs:list T),
+  n < length xs ->
+  splice_nth n (f (nth_default d xs n)) xs = update_nth n f xs.
 Proof.
-  auto.
+  intros.
+  rewrite splice_nth_equiv_update_nth.
+  break_if; auto; omega.
 Qed.
 
-Definition splice_nth {T} n (x:T) xs := firstn n xs ++ x :: skipn (S n) xs.
-Hint Unfold splice_nth.
+Lemma splice_nth_equiv_update_nth_snoc : forall {T} n f d (xs:list T),
+  n >= length xs ->
+  splice_nth n (f (nth_default d xs n)) xs = xs ++ (f d)::nil.
+Proof.
+  intros.
+  rewrite splice_nth_equiv_update_nth.
+  break_if; auto; omega.
+Qed.
+
+Definition IMPOSSIBLE {T} : list T. exact nil. Qed.
+
+Ltac remove_nth_error :=
+  repeat match goal with
+         | _ => exfalso; solve [ eauto using @nth_error_length_not_error ]
+         | [ |- context[match nth_error ?ls ?n with _ => _ end] ]
+           => destruct (nth_error ls n) eqn:?
+         end.
+
+Lemma update_nth_equiv_splice_nth: forall {T} n f (xs:list T),
+  update_nth n f xs =
+  if lt_dec n (length xs)
+  then match nth_error xs n with
+       | Some v => splice_nth n (f v) xs
+       | None => IMPOSSIBLE
+       end
+  else xs.
+Proof.
+  induction n; destruct xs; intros;
+    autorewrite with simpl_update_nth simpl_nth_default in *; simpl in *;
+      try (erewrite IHn; clear IHn); auto.
+  repeat break_match; remove_nth_error; try reflexivity; try omega.
+Qed.
 
 Lemma splice_nth_equiv_set_nth : forall {T} n x (xs:list T),
   splice_nth n x xs =
   if lt_dec n (length xs)
   then set_nth n x xs
   else xs ++ x::nil.
-Proof.
-  induction n, xs; boring.
-  break_if; break_if; auto; omega.
-Qed.
+Proof. intros; rewrite splice_nth_equiv_update_nth with (f := fun _ => x); auto. Qed.
 
 Lemma splice_nth_equiv_set_nth_set : forall {T} n x (xs:list T),
   n < length xs ->
   splice_nth n x xs = set_nth n x xs.
-Proof.
-  intros.
-  rewrite splice_nth_equiv_set_nth.
-  break_if; auto; omega.
-Qed.
+Proof. intros; rewrite splice_nth_equiv_update_nth_update with (f := fun _ => x); auto. Qed.
 
 Lemma splice_nth_equiv_set_nth_snoc : forall {T} n x (xs:list T),
   n >= length xs ->
   splice_nth n x xs = xs ++ x::nil.
-Proof.
-  intros.
-  rewrite splice_nth_equiv_set_nth.
-  break_if; auto; omega.
-Qed.
+Proof. intros; rewrite splice_nth_equiv_update_nth_snoc with (f := fun _ => x); auto. Qed.
 
 Lemma set_nth_equiv_splice_nth: forall {T} n x (xs:list T),
   set_nth n x xs =
@@ -196,11 +418,48 @@ Lemma set_nth_equiv_splice_nth: forall {T} n x (xs:list T),
   then splice_nth n x xs
   else xs.
 Proof.
-  induction n; destruct xs; intros; simpl in *;
-    try (rewrite IHn; clear IHn); auto.
-  break_if; break_if; auto; omega.
+  intros; unfold set_nth; rewrite update_nth_equiv_splice_nth with (f := fun _ => x); auto.
+  repeat break_match; remove_nth_error; trivial.
 Qed.
 
+Lemma combine_update_nth : forall {A B} n f g (xs:list A) (ys:list B),
+  combine (update_nth n f xs) (update_nth n g ys) =
+  update_nth n (fun xy => (f (fst xy), g (snd xy))) (combine xs ys).
+Proof.
+  induction n; destruct xs, ys; simpl; try rewrite IHn; reflexivity.
+Qed.
+
+(* grumble, grumble, [rewrite] is bad at inferring the identity function, and constant functions *)
+Ltac rewrite_rev_combine_update_nth :=
+  let lem := match goal with
+             | [ |- appcontext[update_nth ?n (fun xy => (@?f xy, @?g xy)) (combine ?xs ?ys)] ]
+               => let f := match (eval cbv [fst] in (fun y x => f (x, y))) with
+                           | fun _ => ?f => f
+                           end in
+                  let g := match (eval cbv [snd] in (fun x y => g (x, y))) with
+                           | fun _ => ?g => g
+                           end in
+                  constr:(@combine_update_nth _ _ n f g xs ys)
+             end in
+  rewrite <- lem.
+
+Lemma combine_update_nth_l : forall {A B} n (f : A -> A) xs (ys:list B),
+  combine (update_nth n f xs) ys =
+  update_nth n (fun xy => (f (fst xy), snd xy)) (combine xs ys).
+Proof.
+  intros ??? f xs ys.
+  etransitivity; [ | apply combine_update_nth with (g := fun x => x) ].
+  rewrite update_nth_id; reflexivity.
+Qed.
+
+Lemma combine_update_nth_r : forall {A B} n (g : B -> B) (xs:list A) (ys:list B),
+  combine xs (update_nth n g ys) =
+  update_nth n (fun xy => (fst xy, g (snd xy))) (combine xs ys).
+Proof.
+  intros ??? g xs ys.
+  etransitivity; [ | apply combine_update_nth with (f := fun x => x) ].
+  rewrite update_nth_id; reflexivity.
+Qed.
 
 Lemma combine_set_nth : forall {A B} n (x:A) xs (ys:list B),
   combine (set_nth n x xs) ys =
@@ -209,12 +468,12 @@ Lemma combine_set_nth : forall {A B} n (x:A) xs (ys:list B),
     | Some y => set_nth n (x,y) (combine xs ys)
     end.
 Proof.
-  (* TODO(andreser): this proof can totally be automated, but requires writing ltac that vets multiple hypotheses at once *)
-  induction n, xs, ys; nth_tac; try rewrite IHn; nth_tac;
-    try (f_equal; specialize (IHn x xs ys ); rewrite H in IHn; rewrite <- IHn);
-    try (specialize (nth_error_value_length _ _ _ _ H); omega).
-  assert (Some b0=Some b1) as HA by (rewrite <-H, <-H0; auto).
-  injection HA; intros; subst; auto.
+  intros; unfold set_nth; rewrite combine_update_nth_l.
+  nth_tac;
+    [ repeat rewrite_rev_combine_update_nth; apply f_equal2
+    | assert (nth_error (combine xs ys) n = None)
+      by (apply nth_error_None; rewrite combine_length; omega * ) ];
+    autorewrite with simpl_update_nth; reflexivity.
 Qed.
 
 Lemma nth_error_value_In : forall {T} n xs (x:T),
@@ -258,6 +517,8 @@ Proof.
   destruct (lt_dec n (length xs)); auto.
 Qed.
 
+Hint Rewrite @nth_default_app : push_nth_default.
+
 Lemma combine_truncate_r : forall {A B} (xs : list A) (ys : list B),
   combine xs ys = combine xs (firstn (length xs) ys).
 Proof.
@@ -278,14 +539,34 @@ Proof.
 Qed.
 
 Lemma firstn_nil : forall {A} n, firstn n nil = @nil A.
-Proof.
-  destruct n; auto.
-Qed.
+Proof. destruct n; auto. Qed.
+
+Hint Rewrite @firstn_nil : simpl_firstn.
 
 Lemma skipn_nil : forall {A} n, skipn n nil = @nil A.
-Proof.
-  destruct n; auto.
-Qed.
+Proof. destruct n; auto. Qed.
+
+Hint Rewrite @skipn_nil : simpl_skipn.
+
+Lemma firstn_0 : forall {A} xs, @firstn A 0 xs = nil.
+Proof. reflexivity. Qed.
+
+Hint Rewrite @firstn_0 : simpl_firstn.
+
+Lemma skipn_0 : forall {A} xs, @skipn A 0 xs = xs.
+Proof. reflexivity. Qed.
+
+Hint Rewrite @skipn_0 : simpl_skipn.
+
+Lemma firstn_cons_S : forall {A} n x xs, @firstn A (S n) (x::xs) = x::@firstn A n xs.
+Proof. reflexivity. Qed.
+
+Hint Rewrite @firstn_cons_S : simpl_firstn.
+
+Lemma skipn_cons_S : forall {A} n x xs, @skipn A (S n) (x::xs) = @skipn A n xs.
+Proof. reflexivity. Qed.
+
+Hint Rewrite @skipn_cons_S : simpl_skipn.
 
 Lemma firstn_app : forall {A} n (xs ys : list A),
   firstn n (xs ++ ys) = firstn n xs ++ firstn (n - length xs) ys.
@@ -351,15 +632,12 @@ Proof.
   reflexivity.
 Qed.
 
+Hint Rewrite @fold_right_cons : simpl_fold_right.
+
 Lemma length_cons : forall {T} (x:T) xs, length (x::xs) = S (length xs).
   reflexivity.
 Qed.
 
-Lemma S_pred_nonzero : forall a, (a > 0 -> S (pred a) = a)%nat.
-Proof.
-  destruct a; omega.
-Qed.
-
 Lemma cons_length : forall A (xs : list A) a, length (a :: xs) = S (length xs).
 Proof.
   auto.
@@ -428,17 +706,6 @@ Proof.
   auto.
 Qed.
 
-Lemma nth_default_cons : forall {T} (x u0 : T) us, nth_default x (u0 :: us) 0 = u0.
-Proof.
-  auto.
-Qed.
-
-Lemma nth_default_cons_S : forall {A} us (u0 : A) n d,
-  nth_default d (u0 :: us) (S n) = nth_default d us n.
-Proof.
-  boring.
-Qed.
-
 Lemma nth_error_Some_nth_default : forall {T} i x (l : list T), (i < length l)%nat ->
   nth_error l i = Some (nth_default x l i).
 Proof.
@@ -449,47 +716,52 @@ Proof.
   reflexivity.
 Qed.
 
+Lemma update_nth_cons : forall {T} f (u0 : T) us, update_nth 0 f (u0 :: us) = (f u0) :: us.
+Proof. reflexivity. Qed.
+
+Hint Rewrite @update_nth_cons : simpl_update_nth.
+
 Lemma set_nth_cons : forall {T} (x u0 : T) us, set_nth 0 x (u0 :: us) = x :: us.
-Proof.
-  auto.
-Qed.
+Proof. intros; apply update_nth_cons. Qed.
+
+Hint Rewrite @set_nth_cons : simpl_set_nth.
 
-Create HintDb distr_length discriminated.
 Hint Rewrite
   @nil_length0
   @length_cons
-  @app_length
-  @rev_length
-  @map_length
-  @seq_length
-  @fold_left_length
-  @split_length_l
-  @split_length_r
-  @firstn_length
   @skipn_length
-  @combine_length
-  @prod_length
+  @length_update_nth
   @length_set_nth
   : distr_length.
 Ltac distr_length := autorewrite with distr_length in *;
   try solve [simpl in *; omega].
 
-Lemma cons_set_nth : forall {T} n (x y : T) us,
-  y :: set_nth n x us = set_nth (S n) x (y :: us).
+Lemma cons_update_nth : forall {T} n f (y : T) us,
+  y :: update_nth n f us = update_nth (S n) f (y :: us).
 Proof.
   induction n; boring.
 Qed.
 
-Lemma set_nth_nil : forall {T} n (x : T), set_nth n x nil = nil.
-Proof.
-  induction n; boring.
-Qed.
+Hint Rewrite <- @cons_update_nth : simpl_update_nth.
 
-Lemma nth_default_nil : forall {T} n (d : T), nth_default d nil n = d.
+Lemma update_nth_nil : forall {T} n f, update_nth n f (@nil T) = @nil T.
 Proof.
   induction n; boring.
 Qed.
 
+Hint Rewrite @update_nth_nil : simpl_update_nth.
+
+Lemma cons_set_nth : forall {T} n (x y : T) us,
+  y :: set_nth n x us = set_nth (S n) x (y :: us).
+Proof. intros; apply cons_update_nth. Qed.
+
+Hint Rewrite <- @cons_set_nth : simpl_set_nth.
+
+Lemma set_nth_nil : forall {T} n (x : T), set_nth n x nil = nil.
+Proof. intros; apply update_nth_nil. Qed.
+
+Hint Rewrite @set_nth_nil : simpl_set_nth.
+
 Lemma skipn_nth_default : forall {T} n us (d : T), (n < length us)%nat ->
  skipn n us = nth_default d us n :: skipn (S n) us.
 Proof.
@@ -508,6 +780,8 @@ Proof.
   congruence.
 Qed.
 
+Hint Rewrite @nth_default_out_of_bounds using omega : simpl_nth_default.
+
 Ltac nth_error_inbounds :=
   match goal with
   | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] =>
@@ -535,11 +809,20 @@ Ltac set_nth_inbounds :=
     match goal with
     | [ H : ~ (i < (length xs))%nat |- _ ] => destruct H
     | [ H :   (i < (length xs))%nat |- _ ] => try solve [distr_length]
-    end;
-    idtac
+    end
+  end.
+Ltac update_nth_inbounds :=
+  match goal with
+  | [ |- context[update_nth ?i ?f ?xs] ] =>
+    rewrite (update_nth_equiv_splice_nth i f xs);
+    destruct (lt_dec i (length xs));
+    match goal with
+    | [ H : ~ (i < (length xs))%nat |- _ ] => destruct H
+    | [ H :   (i < (length xs))%nat |- _ ] => remove_nth_error; try solve [distr_length]
+    end
   end.
 
-Ltac nth_inbounds := nth_error_inbounds || set_nth_inbounds.
+Ltac nth_inbounds := nth_error_inbounds || set_nth_inbounds || update_nth_inbounds.
 
 Lemma cons_eq_head : forall {T} (x y:T) xs ys, x::xs = y::ys -> x=y.
 Proof.
@@ -557,6 +840,8 @@ Proof.
   nth_tac.
 Qed.
 
+Hint Rewrite @map_nth_default_always : push_nth_default.
+
 Lemma fold_right_and_True_forall_In_iff : forall {T} (l : list T) (P : T -> Prop),
   (forall x, In x l -> P x) <-> fold_right and True (map P l).
 Proof.
@@ -617,11 +902,236 @@ Proof.
   omega.
 Qed.
 
+Lemma update_nth_out_of_bounds : forall {A} n f xs, n >= length xs -> @update_nth A n f xs = xs.
+Proof.
+  induction n; destruct xs; simpl; try congruence; try omega; intros.
+  rewrite IHn by omega; reflexivity.
+Qed.
+
+Hint Rewrite @update_nth_out_of_bounds using omega : simpl_update_nth.
+
+
+Lemma update_nth_nth_default_full : forall {A} (d:A) n f l i,
+  nth_default d (update_nth n f l) i =
+  if lt_dec i (length l) then
+    if (eq_nat_dec i n) then f (nth_default d l i)
+    else nth_default d l i
+  else d.
+Proof.
+  induction n; (destruct l; simpl in *; [ intros; destruct i; simpl; try reflexivity; omega | ]);
+    intros; repeat break_if; subst; try destruct i;
+      repeat first [ progress break_if
+                   | progress subst
+                   | progress boring
+                   | progress autorewrite with simpl_nth_default
+                   | omega ].
+Qed.
+
+Hint Rewrite @update_nth_nth_default_full : push_nth_default.
+
+Lemma update_nth_nth_default : forall {A} (d:A) n f l i, (0 <= i < length l)%nat ->
+  nth_default d (update_nth n f l) i =
+  if (eq_nat_dec i n) then f (nth_default d l i) else nth_default d l i.
+Proof. intros; rewrite update_nth_nth_default_full; repeat break_if; boring. Qed.
+
+Hint Rewrite @update_nth_nth_default using (omega || distr_length; omega) : push_nth_default.
+
+Lemma set_nth_nth_default_full : forall {A} (d:A) n v l i,
+  nth_default d (set_nth n v l) i =
+  if lt_dec i (length l) then
+    if (eq_nat_dec i n) then v
+    else nth_default d l i
+  else d.
+Proof. intros; apply update_nth_nth_default_full; assumption. Qed.
+
+Hint Rewrite @set_nth_nth_default_full : push_nth_default.
+
 Lemma set_nth_nth_default : forall {A} (d:A) n x l i, (0 <= i < length l)%nat ->
   nth_default d (set_nth n x l) i =
   if (eq_nat_dec i n) then x else nth_default d l i.
+Proof. intros; apply update_nth_nth_default; assumption. Qed.
+
+Hint Rewrite @set_nth_nth_default using (omega || distr_length; omega) : push_nth_default.
+
+Lemma nth_default_preserves_properties : forall {A} (P : A -> Prop) l n d,
+  (forall x, In x l -> P x) -> P d -> P (nth_default d l n).
+Proof.
+  intros; rewrite nth_default_eq.
+  destruct (nth_in_or_default n l d); auto.
+  congruence.
+Qed.
+
+Lemma nth_error_first : forall {T} (a b : T) l,
+  nth_error (a :: l) 0 = Some b -> a = b.
+Proof.
+  intros; simpl in *.
+  unfold value in *.
+  congruence.
+Qed.
+
+Lemma nth_error_exists_first : forall {T} l (x : T) (H : nth_error l 0 = Some x),
+  exists l', l = x :: l'.
+Proof.
+  induction l; try discriminate; eexists.
+  apply nth_error_first in H.
+  subst; eauto.
+Qed.
+
+Lemma list_elementwise_eq : forall {T} (l1 l2 : list T),
+  (forall i, nth_error l1 i = nth_error l2 i) -> l1 = l2.
+Proof.
+  induction l1, l2; intros; try reflexivity;
+    pose proof (H 0%nat) as Hfirst; simpl in Hfirst; inversion Hfirst.
+  f_equal.
+  apply IHl1.
+  intros i; specialize (H (S i)).
+  boring.
+Qed.
+
+Lemma sum_firstn_all_succ : forall n l, (length l <= n)%nat ->
+  sum_firstn l (S n) = sum_firstn l n.
+Proof.
+  unfold sum_firstn; intros.
+  rewrite !firstn_all_strong by omega.
+  congruence.
+Qed.
+
+Hint Rewrite @sum_firstn_all_succ using omega : simpl_sum_firstn.
+
+Lemma sum_firstn_succ_default : forall l i,
+  sum_firstn l (S i) = (nth_default 0 l i + sum_firstn l i)%Z.
+Proof.
+  unfold sum_firstn; induction l, i;
+    intros; autorewrite with simpl_nth_default simpl_firstn simpl_fold_right in *;
+      try reflexivity.
+  rewrite IHl; omega.
+Qed.
+
+Hint Rewrite @sum_firstn_succ_default : simpl_sum_firstn.
+
+Lemma sum_firstn_0 : forall xs,
+  sum_firstn xs 0 = 0%Z.
+Proof.
+  destruct xs; reflexivity.
+Qed.
+
+Hint Rewrite @sum_firstn_0 : simpl_sum_firstn.
+
+Lemma sum_firstn_succ : forall l i x,
+  nth_error l i = Some x ->
+  sum_firstn l (S i) = (x + sum_firstn l i)%Z.
+Proof.
+  intros; rewrite sum_firstn_succ_default.
+  erewrite nth_error_value_eq_nth_default by eassumption; reflexivity.
+Qed.
+
+Hint Rewrite @sum_firstn_succ using congruence : simpl_sum_firstn.
+
+Lemma sum_firstn_succ_default_rev : forall l i,
+  sum_firstn l i = (sum_firstn l (S i) - nth_default 0 l i)%Z.
+Proof.
+  intros; rewrite sum_firstn_succ_default; omega.
+Qed.
+
+Lemma sum_firstn_succ_rev : forall l i x,
+  nth_error l i = Some x ->
+  sum_firstn l i = (sum_firstn l (S i) - x)%Z.
+Proof.
+  intros; erewrite sum_firstn_succ by eassumption; omega.
+Qed.
+
+Lemma nth_default_map2 : forall {A B C} (f : A -> B -> C) ls1 ls2 i d d1 d2,
+  nth_default d (map2 f ls1 ls2) i =
+    if lt_dec i (min (length ls1) (length ls2))
+    then f (nth_default d1 ls1 i) (nth_default d2 ls2 i)
+    else d.
+Proof.
+  induction ls1, ls2.
+  + cbv [map2 length min].
+    intros.
+    break_if; try omega.
+    apply nth_default_nil.
+  + cbv [map2 length min].
+    intros.
+    break_if; try omega.
+    apply nth_default_nil.
+  + cbv [map2 length min].
+    intros.
+    break_if; try omega.
+    apply nth_default_nil.
+  + simpl.
+    destruct i.
+    - intros. rewrite !nth_default_cons.
+      break_if; auto; omega.
+    - intros. rewrite !nth_default_cons_S.
+      rewrite IHls1 with (d1 := d1) (d2 := d2).
+      repeat break_if; auto; omega.
+Qed.
+
+Lemma map2_cons : forall A B C (f : A -> B -> C) ls1 ls2 a b,
+  map2 f (a :: ls1) (b :: ls2) = f a b :: map2 f ls1 ls2.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma map2_nil_l : forall A B C (f : A -> B -> C) ls2,
+  map2 f nil ls2 = nil.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma map2_nil_r : forall A B C (f : A -> B -> C) ls1,
+  map2 f ls1 nil = nil.
+Proof.
+  destruct ls1; reflexivity.
+Qed.
+Local Hint Resolve map2_nil_r map2_nil_l.
+
+Opaque map2.
+
+Lemma map2_length : forall A B C (f : A -> B -> C) ls1 ls2,
+  length (map2 f ls1 ls2) = min (length ls1) (length ls2).
+Proof.
+  induction ls1, ls2; intros; try solve [cbv; auto].
+  rewrite map2_cons, !length_cons, IHls1.
+  auto.
+Qed.
+
+Ltac simpl_list_lengths := repeat match goal with
+  | H : appcontext[length (@nil ?A)] |- _ => rewrite (@nil_length0 A) in H
+  | H : appcontext[length (_ :: _)] |- _ => rewrite length_cons in H
+  | |- appcontext[length (@nil ?A)] => rewrite (@nil_length0 A)
+  | |- appcontext[length (_ :: _)] => rewrite length_cons
+  end.
+
+Lemma map2_app : forall A B C (f : A -> B -> C) ls1 ls2 ls1' ls2',
+  (length ls1 = length ls2) ->
+  map2 f (ls1 ++ ls1') (ls2 ++ ls2') = map2 f ls1 ls2 ++ map2 f ls1' ls2'.
+Proof.
+  induction ls1, ls2; intros; rewrite ?map2_nil_r, ?app_nil_l; try congruence;
+    simpl_list_lengths; try omega.
+  rewrite <-!app_comm_cons, !map2_cons.
+  rewrite IHls1; auto.
+Qed.
+
+Lemma firstn_update_nth {A}
+  : forall f m n (xs : list A), firstn m (update_nth n f xs) = update_nth n f (firstn m xs).
+Proof.
+  induction m; destruct n, xs;
+    autorewrite with simpl_firstn simpl_update_nth;
+    congruence.
+Qed.
+
+Hint Rewrite @firstn_update_nth : push_firstn.
+Hint Rewrite @firstn_update_nth : pull_update_nth.
+Hint Rewrite <- @firstn_update_nth : pull_firstn.
+Hint Rewrite <- @firstn_update_nth : push_update_nth.
+
+Require Import Coq.Lists.SetoidList.
+Global Instance Proper_nth_default : forall A eq,
+  Proper (eq==>eqlistA eq==>Logic.eq==>eq) (nth_default (A:=A)).
 Proof.
-  induction n; (destruct l; [intros; simpl in *; omega | ]); simpl;
-    destruct i; break_if; try omega; intros; try apply nth_default_cons;
-    rewrite !nth_default_cons_S, ?IHn; try break_if; omega || reflexivity.
+  do 5 intro; subst; induction 1.
+  + repeat intro; rewrite !nth_default_nil; assumption.
+  + repeat intro; subst; destruct y0; rewrite ?nth_default_cons, ?nth_default_cons_S; auto.
 Qed.
\ No newline at end of file
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 0cdfd784f..83375f99a 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -1,9 +1,60 @@
+Require Coq.Logic.Eqdep_dec.
 Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega.
 Require Import Coq.micromega.Psatz.
 Import Nat.
 
+Create HintDb natsimplify discriminated.
+
+Hint Resolve mod_bound_pos : arith.
+Hint Resolve (fun x y p q => proj1 (@Nat.mod_bound_pos x y p q)) (fun x y p q => proj2 (@Nat.mod_bound_pos x y p q)) : arith.
+
+Hint Rewrite @mod_small @mod_mod @mod_1_l @mod_1_r succ_pred using omega : natsimplify.
+
 Local Open Scope nat_scope.
 
+Lemma min_def {x y} : min x y = x - (x - y).
+Proof. apply Min.min_case_strong; omega. Qed.
+Lemma max_def {x y} : max x y = x + (y - x).
+Proof. apply Max.max_case_strong; omega. Qed.
+Ltac coq_omega := omega.
+Ltac handle_min_max_for_omega_gen min max :=
+  repeat match goal with
+         | [ H : context[min _ _] |- _ ] => rewrite !min_def in H || setoid_rewrite min_def in H
+         | [ H : context[max _ _] |- _ ] => rewrite !max_def in H || setoid_rewrite max_def in H
+         | [ |- context[min _ _] ] => rewrite !min_def || setoid_rewrite min_def
+         | [ |- context[max _ _] ] => rewrite !max_def || setoid_rewrite max_def
+         end.
+Ltac handle_min_max_for_omega_case_gen min max :=
+  repeat match goal with
+         | [ H : context[min _ _] |- _ ] => revert H
+         | [ H : context[max _ _] |- _ ] => revert H
+         | [ |- context[min _ _] ] => apply Min.min_case_strong
+         | [ |- context[max _ _] ] => apply Max.max_case_strong
+         end;
+  intros.
+Ltac handle_min_max_for_omega := handle_min_max_for_omega_gen min max.
+Ltac handle_min_max_for_omega_case := handle_min_max_for_omega_case_gen min max.
+(* In 8.4, Nat.min is a definition, so we need to unfold it *)
+Ltac handle_min_max_for_omega_compat_84 :=
+  let min := (eval cbv [min] in min) in
+  let max := (eval cbv [max] in max) in
+  handle_min_max_for_omega_gen min max.
+Ltac handle_min_max_for_omega_case_compat_84 :=
+  let min := (eval cbv [min] in min) in
+  let max := (eval cbv [max] in max) in
+  handle_min_max_for_omega_case_gen min max.
+Ltac omega_with_min_max :=
+  handle_min_max_for_omega;
+  try handle_min_max_for_omega_compat_84;
+  omega.
+Ltac omega_with_min_max_case :=
+  handle_min_max_for_omega_case;
+  try handle_min_max_for_omega_case_compat_84;
+  omega.
+Tactic Notation "omega" := coq_omega.
+Tactic Notation "omega" "*" := omega_with_min_max_case.
+Tactic Notation "omega" "**" := omega_with_min_max.
+
 Lemma div_minus : forall a b, b <> 0 -> (a + b) / b = a / b + 1.
 Proof.
   intros.
@@ -86,3 +137,53 @@ Proof.
 Qed.
 
 Hint Resolve pow_nonzero : arith.
+
+Lemma S_pred_nonzero : forall a, (a > 0 -> S (pred a) = a)%nat.
+Proof.
+  destruct a; simpl; omega.
+Qed.
+
+Hint Rewrite S_pred_nonzero using omega : natsimplify.
+
+Lemma mod_same_eq a b : a <> 0 -> a = b -> b mod a = 0.
+Proof. intros; subst; apply mod_same; assumption. Qed.
+
+Hint Rewrite @mod_same_eq using omega : natsimplify.
+Hint Resolve mod_same_eq : arith.
+
+Lemma mod_mod_eq a b c : a <> 0 -> b = c mod a -> b mod a = b.
+Proof. intros; subst; autorewrite with natsimplify; reflexivity. Qed.
+
+Hint Rewrite @mod_mod_eq using (reflexivity || omega) : natsimplify.
+
+Local Arguments minus !_ !_.
+
+Lemma S_mod_full a b : a <> 0 -> (S b) mod a = if eq_nat_dec (S (b mod a)) a
+                                               then 0
+                                               else S (b mod a).
+Proof.
+  change (S b) with (1+b); intros.
+  pose proof (mod_bound_pos b a).
+  rewrite add_mod by assumption.
+  destruct (eq_nat_dec (S (b mod a)) a) as [H'|H'];
+    destruct a as [|[|a]]; autorewrite with natsimplify in *;
+      try congruence; try reflexivity.
+Qed.
+
+Hint Rewrite S_mod_full using omega : natsimplify.
+
+Lemma S_mod a b : a <> 0 -> S (b mod a) <> a -> (S b) mod a = S (b mod a).
+Proof.
+  intros; rewrite S_mod_full by assumption.
+  edestruct eq_nat_dec; omega.
+Qed.
+
+Hint Rewrite S_mod using (omega || autorewrite with natsimplify; omega) : natsimplify.
+
+Lemma eq_nat_dec_refl x : eq_nat_dec x x = left (Logic.eq_refl x).
+Proof.
+  edestruct eq_nat_dec; try congruence.
+  apply f_equal, Eqdep_dec.UIP_dec, eq_nat_dec.
+Qed.
+
+Hint Rewrite eq_nat_dec_refl : natsimplify.
diff --git a/src/Util/Notations.v b/src/Util/Notations.v
index c3f776766..4526e6dce 100644
--- a/src/Util/Notations.v
+++ b/src/Util/Notations.v
@@ -16,8 +16,8 @@ Reserved Notation "x ^ 2" (at level 30, format "x ^ 2").
 Reserved Notation "x ^ 3" (at level 30, format "x ^ 3").
 Reserved Infix "mod" (at level 40, no associativity).
 Reserved Notation "'canonical' 'encoding' 'of' T 'as' B" (at level 50).
-Reserved Infix "<<" (at level 50).
-Reserved Infix "&" (at level 50).
-Reserved Infix "<<" (at level 50).
+Reserved Infix "<<" (at level 30, no associativity).
+Reserved Infix ">>" (at level 30, no associativity).
 Reserved Infix "&" (at level 50).
+Reserved Infix "∣" (at level 50).
 Reserved Infix "~=" (at level 70).
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
index 10ce148b0..c16b87639 100644
--- a/src/Util/NumTheoryUtil.v
+++ b/src/Util/NumTheoryUtil.v
@@ -66,7 +66,7 @@ Qed.
 
 Lemma p_odd : Z.odd p = true.
 Proof.
-  pose proof (prime_odd_or_2 p prime_p).
+  pose proof (Z.prime_odd_or_2 p prime_p).
   destruct H; auto.
 Qed.
 
@@ -124,12 +124,12 @@ Proof.
   assert (b mod p <> 0) as b_nonzero. {
     intuition.
     rewrite <- Z.pow_2_r in a_square.
-    rewrite mod_exp_0 in a_square by prime_bound.
+    rewrite Z.mod_exp_0 in a_square by prime_bound.
     rewrite <- a_square in a_nonzero.
     auto.
   }
   pose proof (squared_fermat_little b b_nonzero).
-  rewrite mod_pow in * by prime_bound.
+  rewrite Z.mod_pow in * by prime_bound.
   rewrite <- a_square.
   rewrite Z.mod_mod; prime_bound.
 Qed.
@@ -172,10 +172,10 @@ Proof.
   intros.
   destruct (exists_primitive_root_power) as [y [in_ZPGroup_y [y_order gpow_y]]]; auto.
   destruct (gpow_y a a_range) as [j [j_range pow_y_j]]; clear gpow_y.
-  rewrite mod_pow in pow_a_x by prime_bound.
+  rewrite Z.mod_pow in pow_a_x by prime_bound.
   replace a with (a mod p) in pow_y_j by (apply Z.mod_small; omega).
   rewrite <- pow_y_j in pow_a_x.
-  rewrite <- mod_pow in pow_a_x by prime_bound.
+  rewrite <- Z.mod_pow in pow_a_x by prime_bound.
   rewrite <- Z.pow_mul_r in pow_a_x by omega.
   assert (p - 1 | j * x) as divide_mul_j_x. {
     rewrite <- phi_is_order in y_order.
@@ -193,13 +193,13 @@ Proof.
   rewrite <- Z_div_plus by omega.
   rewrite Z.mul_comm.
   rewrite x_id_inv in divide_mul_j_x; auto.
-  apply (divide_mul_div _ j 2) in divide_mul_j_x;
+  apply (Z.divide_mul_div _ j 2) in divide_mul_j_x;
     try (apply prime_pred_divide2 || prime_bound); auto.
   rewrite <- Zdivide_Zdiv_eq by (auto || omega).
   rewrite Zplus_diag_eq_mult_2.
   replace (a mod p) with a in pow_y_j by (symmetry; apply Z.mod_small; omega).
   rewrite Z_div_mult by omega; auto.
-  apply divide2_even_iff.
+  apply Z.divide2_even_iff.
   apply prime_pred_even.
 Qed.
 
@@ -281,7 +281,7 @@ Lemma div2_p_1mod4 : forall (p : Z) (prime_p : prime p) (neq_p_2: p <> 2),
   (p / 2) * 2 + 1 = p.
 Proof.
   intros.
-  destruct (prime_odd_or_2 p prime_p); intuition.
+  destruct (Z.prime_odd_or_2 p prime_p); intuition.
   rewrite <- Zdiv2_div.
   pose proof (Zdiv2_odd_eqn p); break_if; congruence || omega.
 Qed.
diff --git a/src/Util/Option.v b/src/Util/Option.v
index db4b69dde..2c11771ff 100644
--- a/src/Util/Option.v
+++ b/src/Util/Option.v
@@ -60,3 +60,12 @@ Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect
          | [ |- context[option_rect ?P ?S ?N (Some ?x) ] ]
            => change (option_rect P S N (Some x)) with (S x); cbv beta
          end.
+
+Definition option_eq {A} eq (x y : option A) :=
+  match x with
+  | None    => y = None
+  | Some ax => match y with
+               | None => False
+               | Some ay => eq ax ay
+               end
+  end.
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index ab98bb7f2..83ec603a0 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -7,6 +7,9 @@ Tactic Notation "test" tactic3(tac) :=
 (** [not tac] is equivalent to [fail tac "succeeds"] if [tac] succeeds, and is equivalent to [idtac] if [tac] fails *)
 Tactic Notation "not" tactic3(tac) := try ((test tac); fail 1 tac "succeeds").
 
+Ltac get_goal :=
+  match goal with |- ?G => G end.
+
 (** find the head of the given expression *)
 Ltac head expr :=
   match expr with
@@ -270,3 +273,30 @@ Ltac side_conditions_before_to_side_conditions_after tac_in H :=
        here, after evars are instantiated, and not above. *)
     move H after H'; clear H'
   | .. ].
+
+(** Do something with every hypothesis. *)
+Ltac do_with_hyp' tac :=
+  match goal with
+    | [ H : _ |- _ ] => tac H
+  end.
+
+(** Rewrite with any applicable hypothesis. *)
+Tactic Notation "rewrite_hyp" "*" := do_with_hyp' ltac:(fun H => rewrite H).
+Tactic Notation "rewrite_hyp" "->" "*" := do_with_hyp' ltac:(fun H => rewrite -> H).
+Tactic Notation "rewrite_hyp" "<-" "*" := do_with_hyp' ltac:(fun H => rewrite <- H).
+Tactic Notation "rewrite_hyp" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite !H).
+Tactic Notation "rewrite_hyp" "->" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite -> !H).
+Tactic Notation "rewrite_hyp" "<-" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite <- !H).
+Tactic Notation "rewrite_hyp" "!*" := progress rewrite_hyp ?*.
+Tactic Notation "rewrite_hyp" "->" "!*" := progress rewrite_hyp -> ?*.
+Tactic Notation "rewrite_hyp" "<-" "!*" := progress rewrite_hyp <- ?*.
+
+Tactic Notation "rewrite_hyp" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite H in * ).
+Tactic Notation "rewrite_hyp" "->" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite -> H in * ).
+Tactic Notation "rewrite_hyp" "<-" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite <- H in * ).
+Tactic Notation "rewrite_hyp" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite !H in * ).
+Tactic Notation "rewrite_hyp" "->" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite -> !H in * ).
+Tactic Notation "rewrite_hyp" "<-" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite <- !H in * ).
+Tactic Notation "rewrite_hyp" "!*" "in" "*" := progress rewrite_hyp ?* in *.
+Tactic Notation "rewrite_hyp" "->" "!*" "in" "*" := progress rewrite_hyp -> ?* in *.
+Tactic Notation "rewrite_hyp" "<-" "!*" "in" "*" := progress rewrite_hyp <- ?* in *.
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 4232c7bf8..13f8bd386 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -166,7 +166,9 @@ end.
 Lemma from_list_default'_eq : forall {T} (d : T) xs n y pf,
   from_list_default' d y n xs = from_list' y n xs pf.
 Proof.
-  induction xs; destruct n; intros; simpl in *; congruence.
+  induction xs; destruct n; intros; simpl in *;
+    solve [ congruence (* 8.5 *)
+          | erewrite IHxs; reflexivity ]. (* 8.4 *)
 Qed.
 
 Lemma from_list_default_eq : forall {T} (d : T) xs n pf,
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index a8b18ffef..2bcbabaac 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1,10 +1,15 @@
 Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv.
 Require Import Coq.omega.Omega Coq.micromega.Psatz Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
 Require Import Crypto.Util.NatUtil.
+Require Import Crypto.Util.Notations.
 Require Import Coq.Lists.List.
 Import Nat.
 Local Open Scope Z.
 
+Infix ">>" := Z.shiftr : Z_scope.
+Infix "<<" := Z.shiftl : Z_scope.
+Infix "&" := Z.land : Z_scope.
+
 Hint Extern 1 => lia : lia.
 Hint Extern 1 => lra : lra.
 Hint Extern 1 => nia : nia.
@@ -17,7 +22,7 @@ Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z
     this database. *)
 Create HintDb zsimplify discriminated.
 Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r : zsimplify.
-Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l using lia : zsimplify.
+Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add Z.div_0_l using lia : zsimplify.
 
 (** "push" means transform [-f x] to [f (-x)]; "pull" means go the other way *)
 Create HintDb push_Zopp discriminated.
@@ -43,318 +48,326 @@ Hint Rewrite Z.div_small_iff using lia : zstrip_div.
     We'll put, e.g., [mul_div_eq] into it below. *)
 Create HintDb zstrip_div.
 
-Lemma gt_lt_symmetry: forall n m, n > m <-> m < n.
-Proof.
-  intros; split; omega.
-Qed.
-
-Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0.
-Proof.
-  intros; omega.
-Qed.
-Hint Resolve positive_is_nonzero.
-
-Lemma div_positive_gt_0 : forall a b, a > 0 -> b > 0 -> a mod b = 0 ->
-  a / b > 0.
-Proof.
-  intros; rewrite gt_lt_symmetry.
-  apply Z.div_str_pos.
-  split; intuition.
-  apply Z.divide_pos_le; try (apply Zmod_divide); omega.
-Qed.
-
-Lemma elim_mod : forall a b m, a = b -> a mod m = b mod m.
-Proof.
-  intros; subst; auto.
-Qed.
-Hint Resolve elim_mod.
-
-Lemma mod_mult_plus: forall a b c, (b <> 0) -> (a * b + c) mod b = c mod b.
-Proof.
-  intros.
-  rewrite Zplus_mod.
-  rewrite Z.mod_mul; auto; simpl.
-  rewrite Zmod_mod; auto.
-Qed.
-
-Lemma pos_pow_nat_pos : forall x n,
-  Z.pos x ^ Z.of_nat n > 0.
-  do 2 (intros; induction n; subst; simpl in *; auto with zarith).
-  rewrite <- Pos.add_1_r, Zpower_pos_is_exp.
-  apply Zmult_gt_0_compat; auto; reflexivity.
-Qed.
-
-Lemma Z_div_mul' : forall a b : Z, b <> 0 -> (b * a) / b = a.
-  intros. rewrite Z.mul_comm. apply Z.div_mul; auto.
-Qed.
-
-Hint Rewrite Z_div_mul' using lia : zsimplify.
-
-Lemma Zgt0_neq0 : forall x, x > 0 -> x <> 0.
-  intuition.
-Qed.
-
-Lemma pow_Z2N_Zpow : forall a n, 0 <= a ->
-  ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat.
-Proof.
-  intros; induction n; try reflexivity.
-  rewrite Nat2Z.inj_succ.
-  rewrite pow_succ_r by apply le_0_n.
-  rewrite Z.pow_succ_r by apply Zle_0_nat.
-  rewrite IHn.
-  rewrite Z2Nat.inj_mul; auto using Z.pow_nonneg.
-Qed.
-
-Lemma pow_Zpow : forall a n : nat, Z.of_nat (a ^ n) = Z.of_nat a ^ Z.of_nat n.
-Proof with auto using Zle_0_nat, Z.pow_nonneg.
-  intros; apply Z2Nat.inj...
-  rewrite <- pow_Z2N_Zpow, !Nat2Z.id...
-Qed.
-
-Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 ->
-  a ^ x mod m = 0.
-Proof.
-  intros.
-  replace x with (Z.of_nat (Z.to_nat x)) in * by (apply Z2Nat.id; omega).
-  induction (Z.to_nat x). {
-    simpl in *; omega.
-  } {
-    rewrite Nat2Z.inj_succ in *.
-    rewrite Z.pow_succ_r by omega.
-    rewrite Z.mul_mod by omega.
-    case_eq n; intros. {
-      subst. simpl.
-      rewrite Zmod_1_l by omega.
-      rewrite H1.
-      apply Zmod_0_l.
+Module Z.
+  Definition pow2_mod n i := (n & (Z.ones i)).
+
+  Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0.
+  Proof. intros; omega. Qed.
+
+  Hint Resolve positive_is_nonzero : zarith.
+
+  Lemma div_positive_gt_0 : forall a b, a > 0 -> b > 0 -> a mod b = 0 ->
+    a / b > 0.
+  Proof.
+    intros; rewrite Z.gt_lt_iff.
+    apply Z.div_str_pos.
+    split; intuition.
+    apply Z.divide_pos_le; try (apply Zmod_divide); omega.
+  Qed.
+
+  Lemma elim_mod : forall a b m, a = b -> a mod m = b mod m.
+  Proof. intros; subst; auto. Qed.
+
+  Hint Resolve elim_mod : zarith.
+
+  Lemma mod_add_l : forall a b c, b <> 0 -> (a * b + c) mod b = c mod b.
+  Proof. intros; rewrite (Z.add_comm _ c); autorewrite with zsimplify; reflexivity. Qed.
+  Hint Rewrite mod_add_l using lia : zsimplify.
+
+  Lemma mod_add' : forall a b c, b <> 0 -> (a + b * c) mod b = a mod b.
+  Proof. intros; rewrite (Z.mul_comm _ c); autorewrite with zsimplify; reflexivity. Qed.
+  Lemma mod_add_l' : forall a b c, a <> 0 -> (a * b + c) mod a = c mod a.
+  Proof. intros; rewrite (Z.mul_comm _ b); autorewrite with zsimplify; reflexivity. Qed.
+  Hint Rewrite mod_add' mod_add_l' using lia : zsimplify.
+
+  Lemma pos_pow_nat_pos : forall x n,
+    Z.pos x ^ Z.of_nat n > 0.
+  Proof.
+    do 2 (intros; induction n; subst; simpl in *; auto with zarith).
+    rewrite <- Pos.add_1_r, Zpower_pos_is_exp.
+    apply Zmult_gt_0_compat; auto; reflexivity.
+  Qed.
+
+  Lemma div_mul' : forall a b : Z, b <> 0 -> (b * a) / b = a.
+  Proof. intros. rewrite Z.mul_comm. apply Z.div_mul; auto. Qed.
+  Hint Rewrite div_mul' using lia : zsimplify.
+
+  (** TODO: Should we get rid of this duplicate? *)
+  Notation gt0_neq0 := positive_is_nonzero (only parsing).
+
+  Lemma pow_Z2N_Zpow : forall a n, 0 <= a ->
+    ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat.
+  Proof.
+    intros; induction n; try reflexivity.
+    rewrite Nat2Z.inj_succ.
+    rewrite pow_succ_r by apply le_0_n.
+    rewrite Z.pow_succ_r by apply Zle_0_nat.
+    rewrite IHn.
+    rewrite Z2Nat.inj_mul; auto using Z.pow_nonneg.
+  Qed.
+
+  Lemma pow_Zpow : forall a n : nat, Z.of_nat (a ^ n) = Z.of_nat a ^ Z.of_nat n.
+  Proof with auto using Zle_0_nat, Z.pow_nonneg.
+    intros; apply Z2Nat.inj...
+    rewrite <- pow_Z2N_Zpow, !Nat2Z.id...
+  Qed.
+
+  Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 ->
+    a ^ x mod m = 0.
+  Proof.
+    intros.
+    replace x with (Z.of_nat (Z.to_nat x)) in * by (apply Z2Nat.id; omega).
+    induction (Z.to_nat x). {
+      simpl in *; omega.
+    } {
+      rewrite Nat2Z.inj_succ in *.
+      rewrite Z.pow_succ_r by omega.
+      rewrite Z.mul_mod by omega.
+      case_eq n; intros. {
+        subst. simpl.
+        rewrite Zmod_1_l by omega.
+        rewrite H1.
+        apply Zmod_0_l.
+      } {
+        subst.
+        rewrite IHn by (rewrite Nat2Z.inj_succ in *; omega).
+        rewrite H1.
+        auto.
+      }
+    }
+  Qed.
+
+  Lemma mod_pow : forall (a m b : Z), (0 <= b) -> (m <> 0) ->
+      a ^ b mod m = (a mod m) ^ b mod m.
+  Proof.
+    intros; rewrite <- (Z2Nat.id b) by auto.
+    induction (Z.to_nat b); auto.
+    rewrite Nat2Z.inj_succ.
+    do 2 rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg.
+    rewrite Z.mul_mod by auto.
+    rewrite (Z.mul_mod (a mod m) ((a mod m) ^ Z.of_nat n) m) by auto.
+    rewrite <- IHn by auto.
+    rewrite Z.mod_mod by auto.
+    reflexivity.
+  Qed.
+
+  Ltac divide_exists_mul := let k := fresh "k" in
+  match goal with
+  | [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H; destruct H as [k H]
+  | [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides
+  end; (omega || auto).
+
+  Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0),
+    (a | b * (a / c)) -> (c | a) -> (c | b).
+  Proof.
+    intros ? ? ? ? ? divide_a divide_c_a; do 2 divide_exists_mul.
+    rewrite divide_c_a in divide_a.
+    rewrite div_mul' in divide_a by auto.
+    replace (b * k) with (k * b) in divide_a by ring.
+    replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring.
+    rewrite Z.mul_cancel_l in divide_a by (intuition; rewrite H in divide_c_a; ring_simplify in divide_a; intuition).
+    eapply Zdivide_intro; eauto.
+  Qed.
+
+  Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true.
+  Proof.
+    intro; split. {
+      intro divide2_n.
+      divide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega].
+      rewrite divide2_n.
+      apply Z.even_mul.
     } {
-      subst.
-      rewrite IHn by (rewrite Nat2Z.inj_succ in *; omega).
-      rewrite H1.
-      auto.
+      intro n_even.
+      pose proof (Zmod_even n).
+      rewrite n_even in H.
+      apply Zmod_divide; omega || auto.
     }
-  }
-Qed.
-
-Lemma mod_pow : forall (a m b : Z), (0 <= b) -> (m <> 0) ->
-    a ^ b mod m = (a mod m) ^ b mod m.
-Proof.
-  intros; rewrite <- (Z2Nat.id b) by auto.
-  induction (Z.to_nat b); auto.
-  rewrite Nat2Z.inj_succ.
-  do 2 rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg.
-  rewrite Z.mul_mod by auto.
-  rewrite (Z.mul_mod (a mod m) ((a mod m) ^ Z.of_nat n) m) by auto.
-  rewrite <- IHn by auto.
-  rewrite Z.mod_mod by auto.
-  reflexivity.
-Qed.
-
-Ltac Zdivide_exists_mul := let k := fresh "k" in
-match goal with
-| [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H; destruct H as [k H]
-| [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides
-end; (omega || auto).
-
-Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0),
-  (a | b * (a / c)) -> (c | a) -> (c | b).
-Proof.
-  intros ? ? ? ? ? divide_a divide_c_a; do 2 Zdivide_exists_mul.
-  rewrite divide_c_a in divide_a.
-  rewrite Z_div_mul' in divide_a by auto.
-  replace (b * k) with (k * b) in divide_a by ring.
-  replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring.
-  rewrite Z.mul_cancel_l in divide_a by (intuition; rewrite H in divide_c_a; ring_simplify in divide_a; intuition).
-  eapply Zdivide_intro; eauto.
-Qed.
-
-Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true.
-Proof.
-  intro; split. {
-    intro divide2_n.
-    Zdivide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega].
-    rewrite divide2_n.
-    apply Z.even_mul.
-  } {
-    intro n_even.
-    pose proof (Zmod_even n).
-    rewrite n_even in H.
-    apply Zmod_divide; omega || auto.
-  }
-Qed.
-
-Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true.
-Proof.
-  intros.
-  apply Decidable.imp_not_l; try apply Z.eq_decidable.
-  intros p_neq2.
-  pose proof (Zmod_odd p) as mod_odd.
-  destruct (Sumbool.sumbool_of_bool (Z.odd p)) as [? | p_not_odd]; auto.
-  rewrite p_not_odd in mod_odd.
-  apply Zmod_divides in mod_odd; try omega.
-  destruct mod_odd as [c c_id].
-  rewrite Z.mul_comm in c_id.
-  apply Zdivide_intro in c_id.
-  apply prime_divisors in c_id; auto.
-  destruct c_id; [omega | destruct H; [omega | destruct H; auto]].
-  pose proof (prime_ge_2 p prime_p); omega.
-Qed.
-
-Lemma mul_div_eq : (forall a m, m > 0 -> m * (a / m) = (a - a mod m))%Z.
-Proof.
-  intros.
-  rewrite (Z_div_mod_eq a m) at 2 by auto.
-  ring.
-Qed.
-
-Lemma mul_div_eq' : (forall a m, m > 0 -> (a / m) * m = (a - a mod m))%Z.
-Proof.
-  intros.
-  rewrite (Z_div_mod_eq a m) at 2 by auto.
-  ring.
-Qed.
-
-Hint Rewrite mul_div_eq mul_div_eq' using lia : zdiv_to_mod.
-Hint Rewrite <- mul_div_eq' using lia : zmod_to_div.
-
-Ltac prime_bound := match goal with
-| [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega
-end.
-
-Lemma Zlt_minus_lt_0 : forall n m, m < n -> 0 < n - m.
-Proof.
-  intros; omega.
-Qed.
-
-
-Lemma Z_testbit_low : forall n x i, (0 <= i < n) ->
-  Z.testbit x i = Z.testbit (Z.land x (Z.ones n)) i.
-Proof.
-  intros.
-  rewrite Z.land_ones by omega.
-  symmetry.
-  apply Z.mod_pow2_bits_low.
-  omega.
-Qed.
-
-
-Lemma Z_testbit_shiftl : forall i, (0 <= i) -> forall a b n, (i < n) ->
-  Z.testbit (a + Z.shiftl b n) i = Z.testbit a i.
-Proof.
-  intros.
-  erewrite Z_testbit_low; eauto.
-  rewrite Z.land_ones, Z.shiftl_mul_pow2 by omega.
-  rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 n); omega).
-  auto using Z.mod_pow2_bits_low.
-Qed.
-
-Lemma Z_mod_div_eq0 : forall a b, 0 < b -> (a mod b) / b = 0.
-Proof.
-  intros.
-  apply Z.div_small.
-  auto using Z.mod_pos_bound.
-Qed.
-
-Lemma Z_shiftr_add_land : forall n m a b, (n <= m)%nat ->
-  Z.shiftr ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.of_nat m) = Z.shiftr b (Z.of_nat (m - n)).
-Proof.
-  intros.
-  rewrite Z.land_ones by apply Nat2Z.is_nonneg.
-  rewrite !Z.shiftr_div_pow2 by apply Nat2Z.is_nonneg.
-  rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg.
-  rewrite (le_plus_minus n m) at 1 by assumption.
-  rewrite Nat2Z.inj_add.
-  rewrite Z.pow_add_r by apply Nat2Z.is_nonneg.
-  rewrite <- Z.div_div by first
-    [ pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega
-    | apply Z.pow_pos_nonneg; omega ].
-  rewrite Z.div_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega).
-  rewrite Z_mod_div_eq0 by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega); auto.
-Qed.
-
-Lemma Z_land_add_land : forall n m a b, (m <= n)%nat ->
-  Z.land ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.ones (Z.of_nat m)) = Z.land a (Z.ones (Z.of_nat m)).
-Proof.
-  intros.
-  rewrite !Z.land_ones by apply Nat2Z.is_nonneg.
-  rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg.
-  replace (b * 2 ^ Z.of_nat n) with
-    ((b * 2 ^ Z.of_nat (n - m)) * 2 ^ Z.of_nat m) by
-    (rewrite (le_plus_minus m n) at 2; try assumption;
-     rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg; ring).
-  rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat m)); omega).
-  symmetry. apply Znumtheory.Zmod_div_mod; try (apply Z.pow_pos_nonneg; omega).
-  rewrite (le_plus_minus m n) by assumption.
-  rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg.
-  apply Z.divide_factor_l.
-Qed.
-
-Lemma Z_pow_gt0 : forall a, 0 < a -> forall b, 0 <= b -> 0 < a ^ b.
-Proof.
-  intros until 1.
-  apply natlike_ind; try (simpl; omega).
-  intros.
-  rewrite Z.pow_succ_r by assumption.
-  apply Z.mul_pos_pos; assumption.
-Qed.
-
-Lemma div_pow2succ : forall n x, (0 <= x) ->
-  n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x).
-Proof.
-  intros.
-  rewrite Z.pow_succ_r, Z.mul_comm by auto.
-  rewrite <- Z.div_div by (try apply Z.pow_nonzero; omega).
-  rewrite Zdiv2_div.
-  reflexivity.
-Qed.
-
-Lemma shiftr_succ : forall n x,
-  Z.shiftr n (Z.succ x) = Z.shiftr (Z.shiftr n x) 1.
-Proof.
-  intros.
-  rewrite Z.shiftr_shiftr by omega.
-  reflexivity.
-Qed.
-
-
-Definition Z_shiftl_by n a := Z.shiftl a n.
-
-Lemma Z_shiftl_by_mul_pow2 : forall n a, 0 <= n -> Z.mul (2 ^ n) a = Z_shiftl_by n a.
-Proof.
-  intros.
-  unfold Z_shiftl_by.
-  rewrite Z.shiftl_mul_pow2 by assumption.
-  apply Z.mul_comm.
-Qed.
-
-Lemma map_shiftl : forall n l, 0 <= n -> map (Z.mul (2 ^ n)) l = map (Z_shiftl_by n) l.
-Proof.
-  intros; induction l; auto using Z_shiftl_by_mul_pow2.
-  simpl.
-  rewrite IHl.
-  f_equal.
-  apply Z_shiftl_by_mul_pow2.
-  assumption.
-Qed.
-
-Lemma Z_odd_mod : forall a b, (b <> 0)%Z ->
-  Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a.
-Proof.
-  intros.
-  rewrite Zmod_eq_full by assumption.
-  rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul.
-  case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r.
-Qed.
-
-Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0.
-Proof.
-  intros.
-  replace b with (b - c + c) by ring.
-  rewrite Z.pow_add_r by omega.
-  apply Z_mod_mult.
-Qed.
-
-  Lemma Z_ones_succ : forall x, (0 <= x) ->
+  Qed.
+
+  Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true.
+  Proof.
+    intros.
+    apply Decidable.imp_not_l; try apply Z.eq_decidable.
+    intros p_neq2.
+    pose proof (Zmod_odd p) as mod_odd.
+    destruct (Sumbool.sumbool_of_bool (Z.odd p)) as [? | p_not_odd]; auto.
+    rewrite p_not_odd in mod_odd.
+    apply Zmod_divides in mod_odd; try omega.
+    destruct mod_odd as [c c_id].
+    rewrite Z.mul_comm in c_id.
+    apply Zdivide_intro in c_id.
+    apply prime_divisors in c_id; auto.
+    destruct c_id; [omega | destruct H; [omega | destruct H; auto]].
+    pose proof (prime_ge_2 p prime_p); omega.
+  Qed.
+
+  Lemma mul_div_eq : forall a m, m > 0 -> m * (a / m) = (a - a mod m).
+  Proof.
+    intros.
+    rewrite (Z_div_mod_eq a m) at 2 by auto.
+    ring.
+  Qed.
+
+  Lemma mul_div_eq' : (forall a m, m > 0 -> (a / m) * m = (a - a mod m))%Z.
+  Proof.
+    intros.
+    rewrite (Z_div_mod_eq a m) at 2 by auto.
+    ring.
+  Qed.
+
+  Hint Rewrite mul_div_eq mul_div_eq' using lia : zdiv_to_mod.
+  Hint Rewrite <- mul_div_eq' using lia : zmod_to_div.
+
+  Ltac prime_bound := match goal with
+  | [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega
+  end.
+
+  Lemma testbit_low : forall n x i, (0 <= i < n) ->
+    Z.testbit x i = Z.testbit (Z.land x (Z.ones n)) i.
+  Proof.
+    intros.
+    rewrite Z.land_ones by omega.
+    symmetry.
+    apply Z.mod_pow2_bits_low.
+    omega.
+  Qed.
+
+
+  Lemma testbit_add_shiftl_low : forall i, (0 <= i) -> forall a b n, (i < n) ->
+    Z.testbit (a + Z.shiftl b n) i = Z.testbit a i.
+  Proof.
+    intros.
+    erewrite Z.testbit_low; eauto.
+    rewrite Z.land_ones, Z.shiftl_mul_pow2 by omega.
+    rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 n); omega).
+    auto using Z.mod_pow2_bits_low.
+  Qed.
+
+  Lemma mod_div_eq0 : forall a b, 0 < b -> (a mod b) / b = 0.
+  Proof.
+    intros.
+    apply Z.div_small.
+    auto using Z.mod_pos_bound.
+  Qed.
+  Hint Rewrite mod_div_eq0 using lia : zsimplify.
+
+  Lemma shiftr_add_shiftl_high : forall n m a b, 0 <= n <= m -> 0 <= a < 2 ^ n ->
+    Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr b (m - n).
+  Proof.
+    intros.
+    rewrite !Z.shiftr_div_pow2, Z.shiftl_mul_pow2 by omega.
+    replace (2 ^ m) with (2 ^ n * 2 ^ (m - n)) by
+      (rewrite <-Z.pow_add_r by omega; f_equal; ring).
+    rewrite <-Z.div_div, Z.div_add, (Z.div_small a) ; try solve
+      [assumption || apply Z.pow_nonzero || apply Z.pow_pos_nonneg; omega].
+    f_equal; ring.
+  Qed.
+
+  Lemma shiftr_add_shiftl_low : forall n m a b, 0 <= m <= n -> 0 <= a < 2 ^ n ->
+    Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr a m + Z.shiftr b (m - n).
+  Proof.
+    intros.
+    rewrite !Z.shiftr_div_pow2, Z.shiftl_mul_pow2, Z.shiftr_mul_pow2 by omega.
+    replace (2 ^ n) with (2 ^ (n - m) * 2 ^ m) by
+      (rewrite <-Z.pow_add_r by omega; f_equal; ring).
+    rewrite Z.mul_assoc, Z.div_add by (apply Z.pow_nonzero; omega).
+    repeat f_equal; ring.
+  Qed.
+
+  Lemma testbit_add_shiftl_high : forall i, (0 <= i) -> forall a b n, (0 <= n <= i) ->
+    0 <= a < 2 ^ n ->
+    Z.testbit (a + Z.shiftl b n) i = Z.testbit b (i - n).
+  Proof.
+    intros ? ?.
+    apply natlike_ind with (x := i); intros; try assumption;
+      (destruct (Z_eq_dec 0 n); [ subst; rewrite Z.pow_0_r in *;
+       replace a with 0 by omega; f_equal; ring | ]); try omega.
+    rewrite <-Z.add_1_r at 1. rewrite <-Z.shiftr_spec by assumption.
+    replace (Z.succ x - n) with (x - (n - 1)) by ring.
+    rewrite shiftr_add_shiftl_low, <-Z.shiftl_opp_r with (a := b) by omega.
+    rewrite <-H1 with (a := Z.shiftr a 1); try omega; [ repeat f_equal; ring | ].
+    rewrite Z.shiftr_div_pow2 by omega.
+    split; apply Z.div_pos || apply Z.div_lt_upper_bound;
+      try solve [rewrite ?Z.pow_1_r; omega].
+    rewrite <-Z.pow_add_r by omega.
+    replace (1 + (n - 1)) with n by ring; omega.
+  Qed.
+
+  Lemma land_add_land : forall n m a b, (m <= n)%nat ->
+    Z.land ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.ones (Z.of_nat m)) = Z.land a (Z.ones (Z.of_nat m)).
+  Proof.
+    intros.
+    rewrite !Z.land_ones by apply Nat2Z.is_nonneg.
+    rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg.
+    replace (b * 2 ^ Z.of_nat n) with
+      ((b * 2 ^ Z.of_nat (n - m)) * 2 ^ Z.of_nat m) by
+      (rewrite (le_plus_minus m n) at 2; try assumption;
+       rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg; ring).
+    rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat m)); omega).
+    symmetry. apply Znumtheory.Zmod_div_mod; try (apply Z.pow_pos_nonneg; omega).
+    rewrite (le_plus_minus m n) by assumption.
+    rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg.
+    apply Z.divide_factor_l.
+  Qed.
+
+  Lemma div_pow2succ : forall n x, (0 <= x) ->
+    n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x).
+  Proof.
+    intros.
+    rewrite Z.pow_succ_r, Z.mul_comm by auto.
+    rewrite <- Z.div_div by (try apply Z.pow_nonzero; omega).
+    rewrite Zdiv2_div.
+    reflexivity.
+  Qed.
+
+  Lemma shiftr_succ : forall n x,
+    Z.shiftr n (Z.succ x) = Z.shiftr (Z.shiftr n x) 1.
+  Proof.
+    intros.
+    rewrite Z.shiftr_shiftr by omega.
+    reflexivity.
+  Qed.
+
+
+  Definition shiftl_by n a := Z.shiftl a n.
+
+  Lemma shiftl_by_mul_pow2 : forall n a, 0 <= n -> Z.mul (2 ^ n) a = Z.shiftl_by n a.
+  Proof.
+    intros.
+    unfold Z.shiftl_by.
+    rewrite Z.shiftl_mul_pow2 by assumption.
+    apply Z.mul_comm.
+  Qed.
+
+  Lemma map_shiftl : forall n l, 0 <= n -> map (Z.mul (2 ^ n)) l = map (Z.shiftl_by n) l.
+  Proof.
+    intros; induction l; auto using Z.shiftl_by_mul_pow2.
+    simpl.
+    rewrite IHl.
+    f_equal.
+    apply Z.shiftl_by_mul_pow2.
+    assumption.
+  Qed.
+
+  Lemma odd_mod : forall a b, (b <> 0)%Z ->
+    Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a.
+  Proof.
+    intros.
+    rewrite Zmod_eq_full by assumption.
+    rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul.
+    case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r.
+  Qed.
+
+  Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0.
+  Proof.
+    intros.
+    replace b with (b - c + c) by ring.
+    rewrite Z.pow_add_r by omega.
+    apply Z_mod_mult.
+  Qed.
+  Hint Rewrite mod_same_pow using lia : zsimplify.
+
+  Lemma ones_succ : forall x, (0 <= x) ->
     Z.ones (Z.succ x) = 2 ^ x + Z.ones x.
   Proof.
     unfold Z.ones; intros.
@@ -365,14 +378,14 @@ Qed.
     rewrite Z.pow_succ_r; omega.
   Qed.
 
-  Lemma Z_div_floor : forall a b c, 0 < b -> a < b * (Z.succ c) -> a / b <= c.
+  Lemma div_floor : forall a b c, 0 < b -> a < b * (Z.succ c) -> a / b <= c.
   Proof.
     intros.
     apply Z.lt_succ_r.
     apply Z.div_lt_upper_bound; try omega.
   Qed.
 
-  Lemma Z_shiftr_1_r_le : forall a b, a <= b ->
+  Lemma shiftr_1_r_le : forall a b, a <= b ->
     Z.shiftr a 1 <= Z.shiftr b 1.
   Proof.
     intros.
@@ -380,7 +393,7 @@ Qed.
     apply Z.div_le_mono; omega.
   Qed.
 
-  Lemma Z_ones_pred : forall i, 0 < i -> Z.ones (Z.pred i) = Z.shiftr (Z.ones i) 1.
+  Lemma ones_pred : forall i, 0 < i -> Z.ones (Z.pred i) = Z.shiftr (Z.ones i) 1.
   Proof.
     induction i; [ | | pose proof (Pos2Z.neg_is_neg p) ]; try omega.
     intros.
@@ -394,7 +407,7 @@ Qed.
     f_equal. omega.
   Qed.
 
-  Lemma Z_shiftr_ones' : forall a n, 0 <= a < 2 ^ n -> forall i, (0 <= i) ->
+  Lemma shiftr_ones' : forall a n, 0 <= a < 2 ^ n -> forall i, (0 <= i) ->
     Z.shiftr a i <= Z.ones (n - i) \/ n <= i.
   Proof.
     intros until 1.
@@ -408,17 +421,17 @@ Qed.
       left.
       rewrite shiftr_succ.
       replace (n - Z.succ x) with (Z.pred (n - x)) by omega.
-      rewrite Z_ones_pred by omega.
-      apply Z_shiftr_1_r_le.
+      rewrite Z.ones_pred by omega.
+      apply Z.shiftr_1_r_le.
       assumption.
   Qed.
 
-  Lemma Z_shiftr_ones : forall a n i, 0 <= a < 2 ^ n -> (0 <= i) -> (i <= n) ->
+  Lemma shiftr_ones : forall a n i, 0 <= a < 2 ^ n -> (0 <= i) -> (i <= n) ->
     Z.shiftr a i <= Z.ones (n - i) .
   Proof.
     intros a n i G G0 G1.
     destruct (Z_le_lt_eq_dec i n G1).
-    + destruct (Z_shiftr_ones' a n G i G0); omega.
+    + destruct (Z.shiftr_ones' a n G i G0); omega.
     + subst; rewrite Z.sub_diag.
       destruct (Z_eq_dec a 0).
       - subst; rewrite Z.shiftr_0_l; reflexivity.
@@ -426,7 +439,7 @@ Qed.
         apply Z.log2_lt_pow2; omega.
   Qed.
 
-  Lemma Z_shiftr_upper_bound : forall a n, 0 <= n -> 0 <= a <= 2 ^ n -> Z.shiftr a n <= 1.
+  Lemma shiftr_upper_bound : forall a n, 0 <= n -> 0 <= a <= 2 ^ n -> Z.shiftr a n <= 1.
   Proof.
     intros a ? ? [a_nonneg a_upper_bound].
     apply Z_le_lt_eq_dec in a_upper_bound.
@@ -442,439 +455,465 @@ Qed.
       omega.
   Qed.
 
-(* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *)
-Ltac zero_bounds' :=
-  repeat match goal with
-  | [ |- 0 <= _ + _] => apply Z.add_nonneg_nonneg
-  | [ |- 0 <= _ - _] => apply Z.le_0_sub
-  | [ |- 0 <= _ * _] => apply Z.mul_nonneg_nonneg
-  | [ |- 0 <= _ / _] => apply Z.div_pos
-  | [ |- 0 <= _ ^ _ ] => apply Z.pow_nonneg
-  | [ |- 0 <= Z.shiftr _ _] => apply Z.shiftr_nonneg
-  | [ |- 0 < _ + _] => try solve [apply Z.add_pos_nonneg; zero_bounds'];
-                       try solve [apply Z.add_nonneg_pos; zero_bounds']
-  | [ |- 0 < _ - _] => apply Z.lt_0_sub
-  | [ |- 0 < _ * _] => apply Z.lt_0_mul; left; split
-  | [ |- 0 < _ / _] => apply Z.div_str_pos
-  | [ |- 0 < _ ^ _ ] => apply Z.pow_pos_nonneg
-  end; try omega; try prime_bound; auto.
-
-Ltac zero_bounds := try omega; try prime_bound; zero_bounds'.
-
-Hint Extern 1 => progress zero_bounds : zero_bounds.
-
-Lemma Z_ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i.
-Proof.
-  apply natlike_ind.
-  + unfold Z.ones. simpl; omega.
-  + intros.
-    rewrite Z_ones_succ by assumption.
-    zero_bounds.
-Qed.
-
-Lemma Z_ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i.
-Proof.
-  intros.
-  unfold Z.ones.
-  rewrite Z.shiftl_1_l.
-  apply Z.lt_succ_lt_pred.
-  apply Z.pow_gt_1; omega.
-Qed.
-
-Lemma N_le_1_l : forall p, (1 <= N.pos p)%N.
-Proof.
-  destruct p; cbv; congruence.
-Qed.
-
-Lemma Pos_land_upper_bound_l : forall a b, (Pos.land a b <= N.pos a)%N.
-Proof.
-  induction a; destruct b; intros; try solve [cbv; congruence];
-    simpl; specialize (IHa b); case_eq (Pos.land a b); intro; simpl;
-    try (apply N_le_1_l || apply N.le_0_l); intro land_eq;
-    rewrite land_eq in *; unfold N.le, N.compare in *;
-    rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xO_xO;
-    try assumption.
-  destruct (p ?=a)%positive; cbv; congruence.
-Qed.
-
-Lemma Z_land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) ->
-  Z.land a b <= a.
-Proof.
-  intros.
-  destruct a, b; try solve [exfalso; auto]; try solve [cbv; congruence].
-  cbv [Z.land].
-  rewrite <-N2Z.inj_pos, <-N2Z.inj_le.
-  auto using Pos_land_upper_bound_l.
-Qed.
-
-Lemma Z_land_upper_bound_r : forall a b, (0 <= a) -> (0 <= b) ->
-  Z.land a b <= b.
-Proof.
-  intros.
-  rewrite Z.land_comm.
-  auto using Z_land_upper_bound_l.
-Qed.
-
-Lemma Z_le_fold_right_max : forall low l x, (forall y, In y l -> low <= y) ->
-  In x l -> x <= fold_right Z.max low l.
-Proof.
-  induction l; intros ? lower_bound In_list; [cbv [In] in *; intuition | ].
-  simpl.
-  destruct (in_inv In_list); subst.
-  + apply Z.le_max_l.
-  + etransitivity.
-    - apply IHl; auto; intuition.
-    - apply Z.le_max_r.
-Qed.
-
-Lemma Z_le_fold_right_max_initial : forall low l, low <= fold_right Z.max low l.
-Proof.
-  induction l; intros; try reflexivity.
-  etransitivity; [ apply IHl | apply Z.le_max_r ].
-Qed.
-
-Ltac Zltb_to_Zlt :=
-  repeat match goal with
-         | [ H : (?x <? ?y) = ?b |- _ ]
-           => let H' := fresh in
-              rename H into H';
-              pose proof (Zlt_cases x y) as H;
-              rewrite H' in H;
-              clear H'
-         end.
-
-Ltac Zcompare_to_sgn :=
-  repeat match goal with
-         | [ H : _ |- _ ] => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff in H
-         | _ => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff
-         end.
-
-Local Ltac replace_to_const c :=
-  repeat match goal with
-         | [ H : ?x = ?x |- _ ] => clear H
-         | [ H : ?x = c, H' : context[?x] |- _ ] => rewrite H in H'
-         | [ H : c = ?x, H' : context[?x] |- _ ] => rewrite <- H in H'
-         | [ H : ?x = c |- context[?x] ] => rewrite H
-         | [ H : c = ?x |- context[?x] ] => rewrite <- H
-         end.
-
-Lemma Zlt_div_0 n m : n / m < 0 <-> ((n < 0 < m \/ m < 0 < n) /\ 0 < -(n / m)).
-Proof.
-  Zcompare_to_sgn; rewrite Z.sgn_opp; simpl.
-  pose proof (Zdiv_sgn n m) as H.
-  pose proof (Z.sgn_spec (n / m)) as H'.
-  repeat first [ progress intuition
-               | progress simpl in *
-               | congruence
-               | lia
-               | progress replace_to_const (-1)
-               | progress replace_to_const 0
-               | progress replace_to_const 1
-               | match goal with
-                 | [ x : Z |- _ ] => destruct x
-                 end ].
-Qed.
-
-Lemma two_times_x_minus_x x : 2 * x - x = x.
-Proof. lia. Qed.
-
-Lemma Zmul_div_le x y z
-      (Hx : 0 <= x) (Hy : 0 <= y) (Hz : 0 < z)
-      (Hyz : y <= z)
-  : x * y / z <= x.
-Proof.
-  transitivity (x * z / z); [ | rewrite Z.div_mul by lia; lia ].
-  apply Z_div_le; nia.
-Qed.
-
-Lemma Zdiv_mul_diff a b c
-      (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c)
-  : c * a / b - c * (a / b) <= c.
-Proof.
-  pose proof (Z.mod_pos_bound a b).
-  etransitivity; [ | apply (Zmul_div_le c (a mod b) b); lia ].
-  rewrite (Z_div_mod_eq a b) at 1 by lia.
-  rewrite Z.mul_add_distr_l.
-  replace (c * (b * (a / b))) with ((c * (a / b)) * b) by lia.
-  rewrite Z.div_add_l by lia.
-  lia.
-Qed.
-
-Lemma Zdiv_mul_le_le a b c
-  :  0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b <= c * (a / b) + c.
-Proof.
-  pose proof (Zdiv_mul_diff a b c); split; try apply Z.div_mul_le; lia.
-Qed.
-
-Lemma Zdiv_mul_le_le_offset a b c
-  : 0 <= a -> 0 < b -> 0 <= c -> c * a / b - c <= c * (a / b).
-Proof.
-  pose proof (Zdiv_mul_le_le a b c); lia.
-Qed.
-
-Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Zdiv_mul_le_le_offset Z.add_le_mono Z.sub_le_mono : zarith.
-
-(** * [Zsimplify_fractions_le] *)
-(** The culmination of this series of tactics,
-    [Zsimplify_fractions_le], will use the fact that [a * (b / c) <=
-    (a * b) / c], and do some reasoning modulo associativity and
-    commutativity in [Z] to perform such a reduction.  It may leave
-    over goals if it cannot prove that some denominators are non-zero.
-    If the rewrite [a * (b / c)] → [(a * b) / c] is safe to do on the
-    LHS of the goal, this tactic should not turn a solvable goal into
-    an unsolvable one.
-
-    After running, the tactic does some basic rewriting to simplify
-    fractions, e.g., that [a * b / b = a]. *)
-Ltac Zsplit_sums_step :=
-  match goal with
-  | [ |- _ + _ <= _ ]
-    => etransitivity; [ eapply Z.add_le_mono | ]
-  | [ |- _ - _ <= _ ]
-    => etransitivity; [ eapply Z.sub_le_mono | ]
-  end.
-Ltac Zsplit_sums :=
-  try (Zsplit_sums_step; [ Zsplit_sums.. | ]).
-Ltac Zpre_reorder_fractions_step :=
-  match goal with
-  | [ |- context[?x / ?y * ?z] ]
-    => rewrite (Z.mul_comm (x / y) z)
-  | _ => let LHS := match goal with |- ?LHS <= ?RHS => LHS end in
-         match LHS with
-         | context G[?x * (?y / ?z)]
-           => let G' := context G[(x * y) / z] in
-              transitivity G'
-         end
-  end.
-Ltac Zpre_reorder_fractions :=
-  try first [ Zsplit_sums_step; [ Zpre_reorder_fractions.. | ]
-            | Zpre_reorder_fractions_step; [ .. | Zpre_reorder_fractions ] ].
-Ltac Zsplit_comparison :=
-  match goal with
-  | [ |- ?x <= ?x ] => reflexivity
-  | [ H : _ >= _ |- _ ]
-    => apply Z.ge_le_iff in H
-  | [ |- ?x * ?y <= ?z * ?w ]
-    => lazymatch goal with
-       | [ H : 0 <= x |- _ ] => idtac
-       | [ H : x < 0 |- _ ] => fail
-       | _ => destruct (Z_lt_le_dec x 0)
-       end;
-       [ ..
-       | lazymatch goal with
-         | [ H : 0 <= y |- _ ] => idtac
-         | [ H : y < 0 |- _ ] => fail
-         | _ => destruct (Z_lt_le_dec y 0)
+  Lemma lor_shiftl : forall a b n, 0 <= n -> 0 <= a < 2 ^ n ->
+    Z.lor a (Z.shiftl b n) = a + (Z.shiftl b n).
+  Proof.
+    intros.
+    apply Z.bits_inj'; intros t ?.
+    rewrite Z.lor_spec, Z.shiftl_spec by assumption.
+    destruct (Z_lt_dec t n).
+    + rewrite testbit_add_shiftl_low by omega.
+      rewrite Z.testbit_neg_r with (n := t - n) by omega.
+      apply Bool.orb_false_r.
+    + rewrite testbit_add_shiftl_high by omega.
+      replace (Z.testbit a t) with false; [ apply Bool.orb_false_l | ].
+      symmetry.
+      apply Z.testbit_false; try omega.
+      rewrite Z.div_small; try reflexivity.
+      split; try eapply Z.lt_le_trans with (m := 2 ^ n); try omega.
+      apply Z.pow_le_mono_r; omega.
+  Qed.
+
+  (* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *)
+  Ltac zero_bounds' :=
+    repeat match goal with
+    | [ |- 0 <= _ + _] => apply Z.add_nonneg_nonneg
+    | [ |- 0 <= _ - _] => apply Z.le_0_sub
+    | [ |- 0 <= _ * _] => apply Z.mul_nonneg_nonneg
+    | [ |- 0 <= _ / _] => apply Z.div_pos
+    | [ |- 0 <= _ ^ _ ] => apply Z.pow_nonneg
+    | [ |- 0 <= Z.shiftr _ _] => apply Z.shiftr_nonneg
+    | [ |- 0 <= _ mod _] => apply Z.mod_pos_bound
+    | [ |- 0 < _ + _] => try solve [apply Z.add_pos_nonneg; zero_bounds'];
+                         try solve [apply Z.add_nonneg_pos; zero_bounds']
+    | [ |- 0 < _ - _] => apply Z.lt_0_sub
+    | [ |- 0 < _ * _] => apply Z.lt_0_mul; left; split
+    | [ |- 0 < _ / _] => apply Z.div_str_pos
+    | [ |- 0 < _ ^ _ ] => apply Z.pow_pos_nonneg
+    end; try omega; try prime_bound; auto.
+
+  Ltac zero_bounds := try omega; try prime_bound; zero_bounds'.
+
+  Hint Extern 1 => progress zero_bounds : zero_bounds.
+
+  Lemma ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i.
+  Proof.
+    apply natlike_ind.
+    + unfold Z.ones. simpl; omega.
+    + intros.
+      rewrite Z.ones_succ by assumption.
+      zero_bounds.
+  Qed.
+
+  Lemma ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i.
+  Proof.
+    intros.
+    unfold Z.ones.
+    rewrite Z.shiftl_1_l.
+    apply Z.lt_succ_lt_pred.
+    apply Z.pow_gt_1; omega.
+  Qed.
+
+  Lemma N_le_1_l : forall p, (1 <= N.pos p)%N.
+  Proof.
+    destruct p; cbv; congruence.
+  Qed.
+
+  Lemma Pos_land_upper_bound_l : forall a b, (Pos.land a b <= N.pos a)%N.
+  Proof.
+    induction a; destruct b; intros; try solve [cbv; congruence];
+      simpl; specialize (IHa b); case_eq (Pos.land a b); intro; simpl;
+      try (apply N_le_1_l || apply N.le_0_l); intro land_eq;
+      rewrite land_eq in *; unfold N.le, N.compare in *;
+      rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xO_xO;
+      try assumption.
+    destruct (p ?=a)%positive; cbv; congruence.
+  Qed.
+
+  Lemma land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) ->
+    Z.land a b <= a.
+  Proof.
+    intros.
+    destruct a, b; try solve [exfalso; auto]; try solve [cbv; congruence].
+    cbv [Z.land].
+    rewrite <-N2Z.inj_pos, <-N2Z.inj_le.
+    auto using Pos_land_upper_bound_l.
+  Qed.
+
+  Lemma land_upper_bound_r : forall a b, (0 <= a) -> (0 <= b) ->
+    Z.land a b <= b.
+  Proof.
+    intros.
+    rewrite Z.land_comm.
+    auto using Z.land_upper_bound_l.
+  Qed.
+
+  Lemma le_fold_right_max : forall low l x, (forall y, In y l -> low <= y) ->
+    In x l -> x <= fold_right Z.max low l.
+  Proof.
+    induction l; intros ? lower_bound In_list; [cbv [In] in *; intuition | ].
+    simpl.
+    destruct (in_inv In_list); subst.
+    + apply Z.le_max_l.
+    + etransitivity.
+      - apply IHl; auto; intuition.
+      - apply Z.le_max_r.
+  Qed.
+
+  Lemma le_fold_right_max_initial : forall low l, low <= fold_right Z.max low l.
+  Proof.
+    induction l; intros; try reflexivity.
+    etransitivity; [ apply IHl | apply Z.le_max_r ].
+  Qed.
+
+  Ltac ltb_to_lt :=
+    repeat match goal with
+           | [ H : (?x <? ?y) = ?b |- _ ]
+             => let H' := fresh in
+                rename H into H';
+                pose proof (Zlt_cases x y) as H;
+                rewrite H' in H;
+                clear H'
+           end.
+
+  Ltac compare_to_sgn :=
+    repeat match goal with
+           | [ H : _ |- _ ] => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff in H
+           | _ => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff
+           end.
+
+  Local Ltac replace_to_const c :=
+    repeat match goal with
+           | [ H : ?x = ?x |- _ ] => clear H
+           | [ H : ?x = c, H' : context[?x] |- _ ] => rewrite H in H'
+           | [ H : c = ?x, H' : context[?x] |- _ ] => rewrite <- H in H'
+           | [ H : ?x = c |- context[?x] ] => rewrite H
+           | [ H : c = ?x |- context[?x] ] => rewrite <- H
+           end.
+
+  Lemma lt_div_0 n m : n / m < 0 <-> ((n < 0 < m \/ m < 0 < n) /\ 0 < -(n / m)).
+  Proof.
+    Z.compare_to_sgn; rewrite Z.sgn_opp; simpl.
+    pose proof (Zdiv_sgn n m) as H.
+    pose proof (Z.sgn_spec (n / m)) as H'.
+    repeat first [ progress intuition
+                 | progress simpl in *
+                 | congruence
+                 | lia
+                 | progress replace_to_const (-1)
+                 | progress replace_to_const 0
+                 | progress replace_to_const 1
+                 | match goal with
+                   | [ x : Z |- _ ] => destruct x
+                   end ].
+  Qed.
+
+  Lemma two_times_x_minus_x x : 2 * x - x = x.
+  Proof. lia. Qed.
+
+  Lemma mul_div_le x y z
+        (Hx : 0 <= x) (Hy : 0 <= y) (Hz : 0 < z)
+        (Hyz : y <= z)
+    : x * y / z <= x.
+  Proof.
+    transitivity (x * z / z); [ | rewrite Z.div_mul by lia; lia ].
+    apply Z_div_le; nia.
+  Qed.
+
+  Lemma div_mul_diff a b c
+        (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c)
+    : c * a / b - c * (a / b) <= c.
+  Proof.
+    pose proof (Z.mod_pos_bound a b).
+    etransitivity; [ | apply (mul_div_le c (a mod b) b); lia ].
+    rewrite (Z_div_mod_eq a b) at 1 by lia.
+    rewrite Z.mul_add_distr_l.
+    replace (c * (b * (a / b))) with ((c * (a / b)) * b) by lia.
+    rewrite Z.div_add_l by lia.
+    lia.
+  Qed.
+
+  Lemma div_mul_le_le a b c
+    :  0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b <= c * (a / b) + c.
+  Proof.
+    pose proof (Z.div_mul_diff a b c); split; try apply Z.div_mul_le; lia.
+  Qed.
+
+  Lemma div_mul_le_le_offset a b c
+    : 0 <= a -> 0 < b -> 0 <= c -> c * a / b - c <= c * (a / b).
+  Proof.
+    pose proof (Z.div_mul_le_le a b c); lia.
+  Qed.
+
+  Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Z.div_mul_le_le_offset Z.add_le_mono Z.sub_le_mono : zarith.
+
+  (** * [Z.simplify_fractions_le] *)
+  (** The culmination of this series of tactics,
+      [Z.simplify_fractions_le], will use the fact that [a * (b / c) <=
+      (a * b) / c], and do some reasoning modulo associativity and
+      commutativity in [Z] to perform such a reduction.  It may leave
+      over goals if it cannot prove that some denominators are non-zero.
+      If the rewrite [a * (b / c)] → [(a * b) / c] is safe to do on the
+      LHS of the goal, this tactic should not turn a solvable goal into
+      an unsolvable one.
+
+      After running, the tactic does some basic rewriting to simplify
+      fractions, e.g., that [a * b / b = a]. *)
+  Ltac split_sums_step :=
+    match goal with
+    | [ |- _ + _ <= _ ]
+      => etransitivity; [ eapply Z.add_le_mono | ]
+    | [ |- _ - _ <= _ ]
+      => etransitivity; [ eapply Z.sub_le_mono | ]
+    end.
+  Ltac split_sums :=
+    try (split_sums_step; [ split_sums.. | ]).
+  Ltac pre_reorder_fractions_step :=
+    match goal with
+    | [ |- context[?x / ?y * ?z] ]
+      => rewrite (Z.mul_comm (x / y) z)
+    | _ => let LHS := match goal with |- ?LHS <= ?RHS => LHS end in
+           match LHS with
+           | context G[?x * (?y / ?z)]
+             => let G' := context G[(x * y) / z] in
+                transitivity G'
+           end
+    end.
+  Ltac pre_reorder_fractions :=
+    try first [ split_sums_step; [ pre_reorder_fractions.. | ]
+              | pre_reorder_fractions_step; [ .. | pre_reorder_fractions ] ].
+  Ltac split_comparison :=
+    match goal with
+    | [ |- ?x <= ?x ] => reflexivity
+    | [ H : _ >= _ |- _ ]
+      => apply Z.ge_le_iff in H
+    | [ |- ?x * ?y <= ?z * ?w ]
+      => lazymatch goal with
+         | [ H : 0 <= x |- _ ] => idtac
+         | [ H : x < 0 |- _ ] => fail
+         | _ => destruct (Z_lt_le_dec x 0)
          end;
          [ ..
-         | apply Zmult_le_compat; [ | | assumption | assumption ] ] ]
-  | [ |- ?x / ?y <= ?z / ?y ]
-    => lazymatch goal with
-       | [ H : 0 < y |- _ ] => idtac
-       | [ H : y <= 0 |- _ ] => fail
-       | _ => destruct (Z_lt_le_dec 0 y)
-       end;
-       [ apply Z_div_le; [ apply gt_lt_symmetry; assumption | ]
-       | .. ]
-  | [ |- ?x / ?y <= ?x / ?z ]
-    => lazymatch goal with
-       | [ H : 0 <= x |- _ ] => idtac
-       | [ H : x < 0 |- _ ] => fail
-       | _ => destruct (Z_lt_le_dec x 0)
-       end;
-       [ ..
-       | lazymatch goal with
-         | [ H : 0 < z |- _ ] => idtac
-         | [ H : z <= 0 |- _ ] => fail
-         | _ => destruct (Z_lt_le_dec 0 z)
+         | lazymatch goal with
+           | [ H : 0 <= y |- _ ] => idtac
+           | [ H : y < 0 |- _ ] => fail
+           | _ => destruct (Z_lt_le_dec y 0)
+           end;
+           [ ..
+           | apply Zmult_le_compat; [ | | assumption | assumption ] ] ]
+    | [ |- ?x / ?y <= ?z / ?y ]
+      => lazymatch goal with
+         | [ H : 0 < y |- _ ] => idtac
+         | [ H : y <= 0 |- _ ] => fail
+         | _ => destruct (Z_lt_le_dec 0 y)
          end;
-         [ apply Z.div_le_compat_l; [ assumption | split; [ assumption | ] ]
-         | .. ] ]
-  | [ |- _ + _ <= _ + _ ]
-    => apply Z.add_le_mono
-  | [ |- _ - _ <= _ - _ ]
-    => apply Z.sub_le_mono
-  | [ |- ?x * (?y / ?z) <= (?x * ?y) / ?z ]
-    => apply Z.div_mul_le
-  end.
-Ltac Zsplit_comparison_fin_step :=
-  match goal with
-  | _ => assumption
-  | _ => lia
-  | _ => progress subst
-  | [ H : ?n * ?m < 0 |- _ ]
-    => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [[??]|[??]]
-  | [ H : ?n / ?m < 0 |- _ ]
-    => apply (proj1 (Zlt_div_0 n m)) in H; destruct H as [[[??]|[??]]?]
-  | [ H : (?x^?y) <= ?n < _, H' : ?n < 0 |- _ ]
-    => assert (0 <= x^y) by zero_bounds; lia
-  | [ H : (?x^?y) < 0 |- _ ]
-    => assert (0 <= x^y) by zero_bounds; lia
-  | [ H : (?x^?y) <= 0 |- _ ]
-    => let H' := fresh in
-       assert (H' : 0 <= x^y) by zero_bounds;
-       assert (x^y = 0) by lia;
-       clear H H'
-  | [ H : _^_ = 0 |- _ ]
-    => apply Z.pow_eq_0_iff in H; destruct H as [?|[??]]
-  | [ H : 0 <= ?x, H' : ?x - 1 < 0 |- _ ]
-    => assert (x = 0) by lia; clear H H'
-  | [ |- ?x <= ?y ] => is_evar x; reflexivity
-  | [ |- ?x <= ?y ] => is_evar y; reflexivity
-  end.
-Ltac Zsplit_comparison_fin := repeat Zsplit_comparison_fin_step.
-Ltac Zsimplify_fractions_step :=
-  match goal with
-  | _ => rewrite Z.div_mul by (try apply Z.pow_nonzero; zero_bounds)
-  | [ |- context[?x * ?y / ?x] ]
-    => rewrite (Z.mul_comm x y)
-  | [ |- ?x <= ?x ] => reflexivity
-  end.
-Ltac Zsimplify_fractions := repeat Zsimplify_fractions_step.
-Ltac Zsimplify_fractions_le :=
-  Zpre_reorder_fractions;
-  [ repeat Zsplit_comparison; Zsplit_comparison_fin; zero_bounds..
-  | Zsimplify_fractions ].
-
-Lemma Zlog2_nonneg' n a : n <= 0 -> n <= Z.log2 a.
-Proof.
-  intros; transitivity 0; auto with zarith.
-Qed.
+         [ apply Z_div_le; [ apply Z.gt_lt_iff; assumption | ]
+         | .. ]
+    | [ |- ?x / ?y <= ?x / ?z ]
+      => lazymatch goal with
+         | [ H : 0 <= x |- _ ] => idtac
+         | [ H : x < 0 |- _ ] => fail
+         | _ => destruct (Z_lt_le_dec x 0)
+         end;
+         [ ..
+         | lazymatch goal with
+           | [ H : 0 < z |- _ ] => idtac
+           | [ H : z <= 0 |- _ ] => fail
+           | _ => destruct (Z_lt_le_dec 0 z)
+           end;
+           [ apply Z.div_le_compat_l; [ assumption | split; [ assumption | ] ]
+           | .. ] ]
+    | [ |- _ + _ <= _ + _ ]
+      => apply Z.add_le_mono
+    | [ |- _ - _ <= _ - _ ]
+      => apply Z.sub_le_mono
+    | [ |- ?x * (?y / ?z) <= (?x * ?y) / ?z ]
+      => apply Z.div_mul_le
+    end.
+  Ltac split_comparison_fin_step :=
+    match goal with
+    | _ => assumption
+    | _ => lia
+    | _ => progress subst
+    | [ H : ?n * ?m < 0 |- _ ]
+      => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [[??]|[??]]
+    | [ H : ?n / ?m < 0 |- _ ]
+      => apply (proj1 (lt_div_0 n m)) in H; destruct H as [[[??]|[??]]?]
+    | [ H : (?x^?y) <= ?n < _, H' : ?n < 0 |- _ ]
+      => assert (0 <= x^y) by zero_bounds; lia
+    | [ H : (?x^?y) < 0 |- _ ]
+      => assert (0 <= x^y) by zero_bounds; lia
+    | [ H : (?x^?y) <= 0 |- _ ]
+      => let H' := fresh in
+         assert (H' : 0 <= x^y) by zero_bounds;
+         assert (x^y = 0) by lia;
+         clear H H'
+    | [ H : _^_ = 0 |- _ ]
+      => apply Z.pow_eq_0_iff in H; destruct H as [?|[??]]
+    | [ H : 0 <= ?x, H' : ?x - 1 < 0 |- _ ]
+      => assert (x = 0) by lia; clear H H'
+    | [ |- ?x <= ?y ] => is_evar x; reflexivity
+    | [ |- ?x <= ?y ] => is_evar y; reflexivity
+    end.
+  Ltac split_comparison_fin := repeat split_comparison_fin_step.
+  Ltac simplify_fractions_step :=
+    match goal with
+    | _ => rewrite Z.div_mul by (try apply Z.pow_nonzero; zero_bounds)
+    | [ |- context[?x * ?y / ?x] ]
+      => rewrite (Z.mul_comm x y)
+    | [ |- ?x <= ?x ] => reflexivity
+    end.
+  Ltac simplify_fractions := repeat simplify_fractions_step.
+  Ltac simplify_fractions_le :=
+    pre_reorder_fractions;
+    [ repeat split_comparison; split_comparison_fin; zero_bounds..
+    | simplify_fractions ].
+
+  Lemma log2_nonneg' n a : n <= 0 -> n <= Z.log2 a.
+  Proof.
+    intros; transitivity 0; auto with zarith.
+  Qed.
 
-Hint Resolve Zlog2_nonneg' : zarith.
+  Hint Resolve log2_nonneg' : zarith.
 
-(** We create separate databases for two directions of transformations
-    involving [Z.log2]; combining them leads to loops. *)
-(* for hints that take in hypotheses of type [log2 _], and spit out conclusions of type [_ ^ _] *)
-Create HintDb hyp_log2.
+  (** We create separate databases for two directions of transformations
+      involving [Z.log2]; combining them leads to loops. *)
+  (* for hints that take in hypotheses of type [log2 _], and spit out conclusions of type [_ ^ _] *)
+  Create HintDb hyp_log2.
 
-(* for hints that take in hypotheses of type [_ ^ _], and spit out conclusions of type [log2 _] *)
-Create HintDb concl_log2.
+  (* for hints that take in hypotheses of type [_ ^ _], and spit out conclusions of type [log2 _] *)
+  Create HintDb concl_log2.
 
-Hint Resolve (fun a b H => proj1 (Z.log2_lt_pow2 a b H)) (fun a b H => proj1 (Z.log2_le_pow2 a b H)) : concl_log2.
-Hint Resolve (fun a b H => proj2 (Z.log2_lt_pow2 a b H)) (fun a b H => proj2 (Z.log2_le_pow2 a b H)) : hyp_log2.
+  Hint Resolve (fun a b H => proj1 (Z.log2_lt_pow2 a b H)) (fun a b H => proj1 (Z.log2_le_pow2 a b H)) : concl_log2.
+  Hint Resolve (fun a b H => proj2 (Z.log2_lt_pow2 a b H)) (fun a b H => proj2 (Z.log2_le_pow2 a b H)) : hyp_log2.
 
-Lemma Zle_lt_to_log2 x y z : 0 <= z -> 0 < y -> 2^x <= y < 2^z -> x <= Z.log2 y < z.
-Proof.
-  destruct (Z_le_gt_dec 0 x); auto with concl_log2 lia.
-Qed.
+  Lemma le_lt_to_log2 x y z : 0 <= z -> 0 < y -> 2^x <= y < 2^z -> x <= Z.log2 y < z.
+  Proof.
+    destruct (Z_le_gt_dec 0 x); auto with concl_log2 lia.
+  Qed.
+
+  Lemma div_x_y_x x y : 0 < x -> 0 < y -> x / y / x = 1 / y.
+  Proof.
+    intros; rewrite Z.div_div, (Z.mul_comm y x), <- Z.div_div, Z.div_same by lia.
+    reflexivity.
+  Qed.
 
-Lemma Zdiv_x_y_x x y : 0 < x -> 0 < y -> x / y / x = 1 / y.
-Proof.
-  intros; rewrite Z.div_div, (Z.mul_comm y x), <- Z.div_div, Z.div_same by lia.
-  reflexivity.
-Qed.
+  Hint Rewrite div_x_y_x using lia : zsimplify.
 
-Hint Rewrite Zdiv_x_y_x using lia : zsimplify.
+  Lemma mod_opp_l_z_iff a b (H : b <> 0) : a mod b = 0 <-> (-a) mod b = 0.
+  Proof.
+    split; intro H'; apply Z.mod_opp_l_z in H'; rewrite ?Z.opp_involutive in H'; assumption.
+  Qed.
 
-Lemma Zmod_opp_l_z_iff a b (H : b <> 0) : a mod b = 0 <-> (-a) mod b = 0.
-Proof.
-  split; intro H'; apply Z.mod_opp_l_z in H'; rewrite ?Z.opp_involutive in H'; assumption.
-Qed.
+  Lemma opp_eq_0_iff a : -a = 0 <-> a = 0.
+  Proof. lia. Qed.
 
-Lemma Zopp_eq_0_iff a : -a = 0 <-> a = 0.
-Proof. lia. Qed.
+  Hint Rewrite <- mod_opp_l_z_iff using lia : zsimplify.
+  Hint Rewrite opp_eq_0_iff : zsimplify.
 
-Hint Rewrite <- Zmod_opp_l_z_iff using lia : zsimplify.
-Hint Rewrite Zopp_eq_0_iff : zsimplify.
+  Lemma sub_pos_bound a b X : 0 <= a < X -> 0 <= b < X -> -X < a - b < X.
+  Proof. lia. Qed.
 
-Lemma Zsub_pos_bound a b X : 0 <= a < X -> 0 <= b < X -> -X < a - b < X.
-Proof. lia. Qed.
+  Lemma div_opp_l_complete a b (Hb : b <> 0) : -a/b = -(a/b) - (if Z_zerop (a mod b) then 0 else 1).
+  Proof.
+    destruct (Z_zerop (a mod b)); autorewrite with zsimplify push_Zopp; reflexivity.
+  Qed.
 
-Lemma Zdiv_opp_l_complete a b (Hb : b <> 0) : -a/b = -(a/b) - (if Z_zerop (a mod b) then 0 else 1).
-Proof.
-  destruct (Z_zerop (a mod b)); autorewrite with zsimplify push_Zopp; reflexivity.
-Qed.
+  Lemma div_opp_l_complete' a b (Hb : b <> 0) : -(a/b) = -a/b + (if Z_zerop (a mod b) then 0 else 1).
+  Proof.
+    destruct (Z_zerop (a mod b)); autorewrite with zsimplify pull_Zopp; lia.
+  Qed.
 
-Lemma Zdiv_opp_l_complete' a b (Hb : b <> 0) : -(a/b) = -a/b + (if Z_zerop (a mod b) then 0 else 1).
-Proof.
-  destruct (Z_zerop (a mod b)); autorewrite with zsimplify pull_Zopp; lia.
-Qed.
+  Hint Rewrite Z.div_opp_l_complete using lia : pull_Zopp.
+  Hint Rewrite Z.div_opp_l_complete' using lia : push_Zopp.
 
-Hint Rewrite Zdiv_opp_l_complete using lia : pull_Zopp.
-Hint Rewrite Zdiv_opp_l_complete' using lia : push_Zopp.
+  Lemma div_opp a : a <> 0 -> -a / a = -1.
+  Proof.
+    intros; autorewrite with pull_Zopp zsimplify; lia.
+  Qed.
 
-Lemma Zdiv_opp a : a <> 0 -> -a / a = -1.
-Proof.
-  intros; autorewrite with pull_Zopp zsimplify; lia.
-Qed.
+  Hint Rewrite Z.div_opp using lia : zsimplify.
 
-Hint Rewrite Zdiv_opp using lia : zsimplify.
+  Lemma div_sub_1_0 x : x > 0 -> (x - 1) / x = 0.
+  Proof. auto with zarith lia. Qed.
 
-Lemma Zdiv_sub_1_0 x : x > 0 -> (x - 1) / x = 0.
-Proof. auto with zarith lia. Qed.
+  Hint Rewrite div_sub_1_0 using lia : zsimplify.
 
-Hint Rewrite Zdiv_sub_1_0 using lia : zsimplify.
+  Lemma sub_pos_bound_div a b X : 0 <= a < X -> 0 <= b < X -> -1 <= (a - b) / X <= 0.
+  Proof.
+    intros H0 H1; pose proof (Z.sub_pos_bound a b X H0 H1).
+    assert (Hn : -X <= a - b) by lia.
+    assert (Hp : a - b <= X - 1) by lia.
+    split; etransitivity; [ | apply Z_div_le, Hn; lia | apply Z_div_le, Hp; lia | ];
+      instantiate; autorewrite with zsimplify; try reflexivity.
+  Qed.
 
-Lemma Zsub_pos_bound_div a b X : 0 <= a < X -> 0 <= b < X -> -1 <= (a - b) / X <= 0.
-Proof.
-  intros H0 H1; pose proof (Zsub_pos_bound a b X H0 H1).
-  assert (Hn : -X <= a - b) by lia.
-  assert (Hp : a - b <= X - 1) by lia.
-  split; etransitivity; [ | apply Z_div_le, Hn; lia | apply Z_div_le, Hp; lia | ];
-    instantiate; autorewrite with zsimplify; try reflexivity.
-Qed.
+  Hint Resolve (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1))
+       (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith.
 
-Hint Resolve (fun a b X H0 H1 => proj1 (Zsub_pos_bound_div a b X H0 H1))
-     (fun a b X H0 H1 => proj1 (Zsub_pos_bound_div a b X H0 H1)) : zarith.
+  Lemma sub_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (a - b) / X = if a <? b then -1 else 0.
+  Proof.
+    intros H0 H1; pose proof (Z.sub_pos_bound_div a b X H0 H1).
+    destruct (a <? b) eqn:?; Z.ltb_to_lt.
+    { cut ((a - b) / X <> 0); [ lia | ].
+      autorewrite with zstrip_div; auto with zarith lia. }
+    { autorewrite with zstrip_div; auto with zarith lia. }
+  Qed.
 
-Lemma Zsub_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (a - b) / X = if a <? b then -1 else 0.
-Proof.
-  intros H0 H1; pose proof (Zsub_pos_bound_div a b X H0 H1).
-  destruct (a <? b) eqn:?; Zltb_to_Zlt.
-  { cut ((a - b) / X <> 0); [ lia | ].
-    autorewrite with zstrip_div; auto with zarith lia. }
-  { autorewrite with zstrip_div; auto with zarith lia. }
-Qed.
+  Lemma add_opp_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (-b + a) / X = if a <? b then -1 else 0.
+  Proof.
+    rewrite !(Z.add_comm (-_)), !Z.add_opp_r.
+    apply Z.sub_pos_bound_div_eq.
+  Qed.
 
-Lemma Zadd_opp_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (-b + a) / X = if a <? b then -1 else 0.
-Proof.
-  rewrite !(Z.add_comm (-_)), !Z.add_opp_r.
-  apply Zsub_pos_bound_div_eq.
-Qed.
+  Hint Rewrite Z.sub_pos_bound_div_eq Z.add_opp_pos_bound_div_eq using lia : zstrip_div.
 
-Hint Rewrite Zsub_pos_bound_div_eq Zadd_opp_pos_bound_div_eq using lia : zstrip_div.
+  Lemma div_small_sym a b : 0 <= a < b -> 0 = a / b.
+  Proof. intros; symmetry; apply Z.div_small; assumption. Qed.
 
-Lemma Zdiv_small_sym a b : 0 <= a < b -> 0 = a / b.
-Proof. intros; symmetry; apply Z.div_small; assumption. Qed.
+  Lemma mod_small_sym a b : 0 <= a < b -> a = a mod b.
+  Proof. intros; symmetry; apply Z.mod_small; assumption. Qed.
 
-Lemma Zmod_small_sym a b : 0 <= a < b -> a = a mod b.
-Proof. intros; symmetry; apply Z.mod_small; assumption. Qed.
+  Hint Resolve div_small_sym mod_small_sym : zarith.
 
-Hint Resolve Zdiv_small_sym Zmod_small_sym : zarith.
+  Lemma div_add' a b c : c <> 0 -> (a + c * b) / c = a / c + b.
+  Proof. intro; rewrite <- Z.div_add, (Z.mul_comm c); try lia. Qed.
 
-Lemma Zdiv_add' a b c : c <> 0 -> (a + c * b) / c = a / c + b.
-Proof. intro; rewrite <- Z.div_add, (Z.mul_comm c); try lia. Qed.
+  Lemma div_add_l' a b c : b <> 0 -> (b * a + c) / b = a + c / b.
+  Proof. intro; rewrite <- Z.div_add_l, (Z.mul_comm b); lia. Qed.
 
-Lemma Zdiv_add_l' a b c : b <> 0 -> (b * a + c) / b = a + c / b.
-Proof. intro; rewrite <- Z.div_add_l, (Z.mul_comm b); lia. Qed.
+  Hint Rewrite div_add_l' div_add' using lia : zsimplify.
 
-Hint Rewrite Zdiv_add_l' Zdiv_add' using lia : zsimplify.
+  Lemma div_add_sub_l a b c d : b <> 0 -> (a * b + c - d) / b = a + (c - d) / b.
+  Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l. Qed.
 
-Lemma Zdiv_add_sub_l a b c d : b <> 0 -> (a * b + c - d) / b = a + (c - d) / b.
-Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l. Qed.
+  Lemma div_add_sub_l' a b c d : b <> 0 -> (b * a + c - d) / b = a + (c - d) / b.
+  Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l'. Qed.
 
-Lemma Zdiv_add_sub_l' a b c d : b <> 0 -> (b * a + c - d) / b = a + (c - d) / b.
-Proof. rewrite <- Z.add_sub_assoc; apply Zdiv_add_l'. Qed.
+  Lemma div_add_sub a b c d : c <> 0 -> (a + b * c - d) / c = (a - d) / c + b.
+  Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l. Qed.
 
-Lemma Zdiv_add_sub a b c d : c <> 0 -> (a + b * c - d) / c = (a - d) / c + b.
-Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Zdiv_add_sub_l. Qed.
+  Lemma div_add_sub' a b c d : c <> 0 -> (a + c * b - d) / c = (a - d) / c + b.
+  Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l'. Qed.
 
-Lemma Zdiv_add_sub' a b c d : c <> 0 -> (a + c * b - d) / c = (a - d) / c + b.
-Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Zdiv_add_sub_l'. Qed.
+  Hint Rewrite Z.div_add_sub Z.div_add_sub' Z.div_add_sub_l Z.div_add_sub_l' using lia : zsimplify.
 
-Hint Rewrite Zdiv_add_sub Zdiv_add_sub' Zdiv_add_sub_l Zdiv_add_sub_l' using lia : zsimplify.
+  Lemma div_mul_skip a b k : 0 < b -> 0 < k -> a * b / k / b = a / k.
+  Proof.
+    intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia.
+    autorewrite with zsimplify; reflexivity.
+  Qed.
 
-Lemma Zdiv_mul_skip a b k : 0 < b -> 0 < k -> a * b / k / b = a / k.
-Proof.
-  intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia.
-  autorewrite with zsimplify; reflexivity.
-Qed.
+  Lemma div_mul_skip' a b k : 0 < b -> 0 < k -> b * a / k / b = a / k.
+  Proof.
+    intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia.
+    autorewrite with zsimplify; reflexivity.
+  Qed.
 
-Lemma Zdiv_mul_skip' a b k : 0 < b -> 0 < k -> b * a / k / b = a / k.
-Proof.
-  intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia.
-  autorewrite with zsimplify; reflexivity.
-Qed.
+  Hint Rewrite Z.div_mul_skip Z.div_mul_skip' using lia : zsimplify.
+End Z.
 
-Hint Rewrite Zdiv_mul_skip Zdiv_mul_skip' using lia : zsimplify.
+Module Export BoundsTactics.
+  Ltac prime_bound := Z.prime_bound.
+  Ltac zero_bounds := Z.zero_bounds.
+End BoundsTactics.