Prove monotonicity properties about zrange

3 files changed, 625 insertions, 267 deletions

diff --git a/src/Util/Bool.v b/src/Util/Bool.v
index fe6ae64e4..fb2038de5 100644
--- a/src/Util/Bool.v
+++ b/src/Util/Bool.v
@@ -103,3 +103,8 @@ Ltac split_andb_in_context := repeat split_andb_in_context_step.
 
 Lemma if_const A (b : bool) (x : A) : (if b then x else x) = x.
 Proof. case b; reflexivity. Qed.
+
+Lemma ex_bool_iff_or P : @ex bool P <-> (or (P true) (P false)).
+Proof.
+  split; [ intros [ [] ? ] | intros [?|?]; eexists ]; eauto.
+Qed.
diff --git a/src/Util/ZRange/CornersMonotoneBounds.v b/src/Util/ZRange/CornersMonotoneBounds.v
index 5edeee5e8..9cea5c376 100644
--- a/src/Util/ZRange/CornersMonotoneBounds.v
+++ b/src/Util/ZRange/CornersMonotoneBounds.v
@@ -10,7 +10,9 @@ Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.ZRange.Operations.
 Require Import Crypto.Util.ZRange.BasicLemmas.
+Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.SpecializeAllWays.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.Tactics.SpecializeBy.
@@ -22,332 +24,634 @@ Module ZRange.
   Local Arguments is_bounded_by' !_ _ _ / .
   Local Coercion is_true : bool >-> Sortclass.
 
-  (*Definition extremes_at_boundaries
-             (f : Z -> Z)
-             x_bs
-    : forall x, is_bounded_by_bool x x_bs -> is_bounded_by_bool*)
-
-  Lemma monotone_apply_to_range_genbP
-        (P : Z -> Prop)
-        (f : Z -> zrange)
-        (R := fun b : bool => fun x y => P x /\ P y /\ if b then Z.le x y else Basics.flip Z.le x y)
-        (Hmonotonel : exists b, Proper (R b ==> Z.le) (fun v => lower (f v)))
-        (Hmonotoneu : exists b, Proper (R b ==> Z.le) (fun v => upper (f v)))
-        x_bs x
-        (Hboundedx : is_bounded_by_bool x x_bs)
-        (x_bs_ok : forall xv, is_bounded_by_bool xv x_bs -> P xv)
-    : is_tighter_than_bool (f x) (apply_to_range f x_bs).
+  Fixpoint app' {A B} {n : nat} : nary_T A B (S n) -> tuple' A n -> B
+    := match n with
+       | O => fun f x => f x
+       | S n => fun f '(xs, x) => @app' A B n (f x) xs
+       end.
+  Definition app {A B} {n : nat} : nary_T A B n -> tuple A n -> B
+    := match n with
+       | O => fun x _ => x
+       | S n => @app' A B n
+       end.
+
+  Local Notation R b := (match b with true => Z.le | false => Basics.flip Z.le end).
+
+  Local Notation Rp b := (match b with true => Pos.le | false => Basics.flip Pos.le end).
+
+  Fixpoint is_monotone_on_projections {n : nat} : nary_T Z Z n -> Prop
+    := match n with
+       | O => fun _ => True
+       | S n' => fun f
+                => (forall x, is_monotone_on_projections (f x))
+                  /\ (forall args, exists b, Proper (R b ==> Z.le) (fun x => app (f x) args))
+       end.
+
+  Fixpoint is_piecewise_monotone_on_projections {n : nat} : nary_T Z Z n -> Prop
+    := match n with
+       | O => fun _ => True
+       | S n'
+         => fun f
+            => (forall x, is_piecewise_monotone_on_projections (f x))
+               /\ (forall args, exists b, Proper (Rp b ==> Z.le) (fun x => app (f (Zpos x)) args))
+               /\ (forall args, exists b, Proper (Rp b ==> Z.le) (fun x => app (f (Zneg x)) args))
+       end.
+
+  Definition all_are_bounded_by_bool {n} (v : tuple Z n) (v_bs : tuple zrange n) : bool
+    := Tuple.fieldwiseb is_bounded_by_bool v v_bs.
+
+  Local Ltac fast_split_min_max := rewrite ?Z.min_le_iff, ?Z.max_le_iff.
+
+  Local Ltac t_fin_common_step :=
+    first [ progress cbv [all_are_bounded_by_bool is_bounded_by_bool is_monotone_on_projections is_true is_tighter_than_bool] in *
+          | progress cbv [Proper respectful Basics.flip] in *
+          | progress cbn in *
+          | progress rewrite ?Bool.orb_true_iff, ?Bool.orb_false_iff, ?Bool.andb_true_iff, ?Z.leb_le, ?Z.ltb_lt in *
+          | progress Z.ltb_to_lt
+          | progress fast_split_min_max
+          | progress destruct_head'_and
+          | progress destruct_head'_prod
+          | progress destruct_head'_ex
+          | progress specialize_by exact tt
+          | progress specialize_by exact I
+          | progress destruct_head' zrange
+          | solve [ auto using or_introl, or_intror, Z.le_refl ]
+          | match goal with
+            | [ H : _ -> True |- _ ] => clear H
+            | [ H : ?x <= ?x |- _ ] => clear H
+            | [ H : ?x \/ ?x |- _ ] => assert x by (destruct H; assumption); clear H
+            | [ H : ?x < ?x |- _ ] => exfalso; clear -H; lia
+            | [ H : 0 <= Z.pos _ |- _ ] => clear H
+            | [ H : 0 < Z.pos _ |- _ ] => clear H
+            | [ H : Z.neg _ <= 0 |- _ ] => clear H
+            | [ H : Z.neg _ < 0 |- _ ] => clear H
+            | [ H : Z.pos _ <= Z.neg _ |- _ ] => exfalso; clear -H; lia
+            | [ H : Z.pos _ <= 0 |- _ ] => exfalso; clear -H; lia
+            | [ H : 0 <= Z.neg _ |- _ ] => exfalso; clear -H; lia
+            | [ H : Z.pos _ < 0 |- _ ] => exfalso; clear -H; lia
+            | [ |- context[Z.max 1 (Z.pos ?x)] ] => rewrite (Z.max_r 1 (Zpos x)) by (clear; lia)
+            | [ |- context[Z.min 1 (Z.pos ?x)] ] => rewrite (Z.min_l 1 (Zpos x)) by (clear; lia)
+            | [ H : ?x > ?y |- _ ] => assert (y < x) by (clear -H; lia); clear H
+            | [ H : ?x >= ?y |- _ ] => assert (y <= x) by (clear -H; lia); clear H
+            | [ |- context[Z.max (Z.neg ?x) (-1)] ] => rewrite (Z.max_r (Zneg x) (-1)) by (clear; lia)
+            | [ |- context[Z.min (Z.neg ?x) (-1)] ] => rewrite (Z.min_l (Zneg x) (-1)) by (clear; lia)
+            end ].
+  Local Ltac t_fin_saturate_step :=
+    first [ progress destruct_head'_bool
+          | match goal with
+            | [ H : forall (x : Z) (y : Z), _ <= _ -> _ <= _, v : Z |- _ ]
+              => unique pose proof (H v v ltac:(reflexivity))
+            | [ H : forall (x : Z) (y : Z), _ <= _ -> _ <= _, v : Z, v' : Z |- _ ]
+              => unique pose proof (H v v' ltac:(auto || reflexivity))
+            end
+          | apply conj ].
+  Local Ltac t_fin_specific_pos_step :=
+    first [ match goal with
+            | [ H : _ \/ _ |- _ ] => destruct H as [H|H]; try (exfalso; clear -H; lia); []
+            | [ H : Z.pos _ <= ?v |- _ ] => is_var v; destruct v as [|v|v]; try (exfalso; clear -H; lia)
+            | [ H : ?v <= Z.neg _ |- _ ] => is_var v; destruct v as [|v|v]; try (exfalso; clear -H; lia)
+            | [ H : 0 <= ?v |- _ ] => is_var v; destruct v as [|v|v]; try (exfalso; clear -H; lia)
+            | [ H : ?v <= 0 |- _ ] => is_var v; destruct v as [|v|v]; try (exfalso; clear -H; lia)
+            | [ H : 0 < ?v |- _ ] => is_var v; destruct v as [|v|v]; try (exfalso; clear -H; lia)
+            | [ H : ?v < 0 |- _ ] => is_var v; destruct v as [|v|v]; try (exfalso; clear -H; lia)
+            end
+          | break_innermost_match_step
+          | progress destruct_head'_bool
+          | match goal with
+            | [ H' : Z.le (?f ?p) (?g ?q) |- _ ]
+              => first [ unique assert (Pos.le p q) by (clear -H'; lia)
+                       | unique assert (Pos.le q p) by (clear -H'; lia) ]
+            | [ H : forall x y, Pos.le _ _ -> _ <= _, H' : Pos.le _ _ |- _ ]
+              => unique pose proof (H _ _ H')
+            | [ H : forall x y, Pos.le x _ -> _ <= _, v : positive |- _ ]
+              => unique pose proof (H 1%positive v ltac:(clear; lia))
+            | [ H : forall x y, Pos.le _ x -> _ <= _, v : positive |- _ ]
+              => unique pose proof (H v 1%positive ltac:(clear; lia))
+            end
+          | apply conj
+          | progress destruct_head' Z ].
+  Local Ltac t_fin :=
+    repeat first [ t_fin_common_step
+                 | t_fin_saturate_step ].
+  Local Ltac t_fin_pos :=
+    repeat first [ t_fin_common_step
+                 | t_fin_specific_pos_step ].
+
+  Lemma pull_union_under_args2 A n f g bs
+    : @app' A _ n (under_args2 union f g) bs
+      = union (app' f bs) (app' g bs).
+  Proof. induction n; t_fin. Qed.
+
+  Lemma monotone_n_corners_genb
+        n f
+        (Hmonotone : @is_monotone_on_projections n f)
+        v v_bs
+        (Hboundedx : @all_are_bounded_by_bool n v v_bs)
+    : is_bounded_by_bool (app f v) (app (n_corners f) v_bs).
   Proof.
-    destruct x_bs as [lx ux]; simpl in *.
-    cbv [is_bounded_by_bool is_true is_tighter_than_bool] in *.
-    cbn [lower upper] in *.
-    rewrite !Bool.andb_true_iff, !Z.leb_le_iff in *.
-    setoid_rewrite Bool.andb_true_iff in x_bs_ok.
-    repeat setoid_rewrite Z.leb_le_iff in x_bs_ok.
-    destruct_head'_ex.
-    repeat match goal with
-           | [ H : Proper (R ?b ==> _) _ |- _ ]
-             => unique assert (R b (if b then lx else x) (if b then x else lx)
-                              /\ R b (if b then x else ux) (if b then ux else x))
-               by (unfold R, Basics.flip; destruct b; repeat apply conj; eauto with omega)
-           end.
-    destruct_head' and.
-    repeat match goal with
-           | [ H : Proper (R ?b ==> _) _, H' : R ?b _ _ |- _ ]
-             => unique pose proof (H _ _ H')
-           end.
-    destruct_head bool; split_andb; Z.ltb_to_lt; split_min_max; omega.
+    destruct n as [|n].
+    { cbv [all_are_bounded_by_bool is_bounded_by_bool is_monotone_on_projections is_true] in *; cbn in *.
+      rewrite Bool.andb_true_iff, Z.leb_le; split; reflexivity. }
+    cbv [app tuple all_are_bounded_by_bool fieldwiseb] in *.
+    induction n as [|n IHn].
+    { t_fin. }
+    { destruct v_bs as [ v_bs [l u] ], v as [vs v]; cbn [lower upper] in *.
+      cbn [fieldwiseb' fst snd] in Hboundedx.
+      cbv [is_true] in *.
+      rewrite Bool.andb_true_iff in Hboundedx.
+      destruct Hboundedx as [Hboundedx0 Hboundedx1].
+      destruct Hmonotone as [Hmonotone0 Hmonotone1].
+      specialize (fun x => IHn (f x) (Hmonotone0 _) vs v_bs Hboundedx0).
+      cbn [app'].
+      set (Sn := S n) in *.
+      cbn [n_corners].
+      set (f' := fun x => @n_corners Sn (f x)).
+      lazymatch type of IHn with
+      | forall x, is_bounded_by_bool (@?B x) (app' _ ?v_bs) = true
+        => change (forall x, is_bounded_by_bool (B x) (app' (f' x) v_bs) = true) in IHn
+      end; cbv beta in *.
+      clearbody f'.
+      cbn -[Sn] in *.
+      rewrite pull_union_under_args2.
+      cbv [is_bounded_by_bool app] in *.
+      unfold Sn in Hmonotone1.
+      setoid_rewrite Bool.andb_true_iff in IHn.
+      rewrite ?Bool.andb_true_iff in *.
+      setoid_rewrite Z.leb_le in IHn.
+      rewrite !Z.leb_le in *.
+      specialize (Hmonotone1 vs).
+      destruct Hmonotone1 as [? Hmonotone1].
+      clear -IHn Hboundedx1 Hmonotone1.
+      cbn [lower upper] in *.
+      destruct_head'_bool.
+      all: split; etransitivity; [ | eapply Hmonotone1, Hboundedx1 | eapply Hmonotone1, Hboundedx1 | ].
+      all: first [ etransitivity; [ eapply IHn | ] | etransitivity; [ | eapply IHn ] ].
+      all: clear; t_fin. }
   Qed.
 
-  Lemma monotone_apply_to_range_genb
-        (f : Z -> zrange)
-        (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
-        (Hmonotonel : exists b, Proper (R b ==> Z.le) (fun v => lower (f v)))
-        (Hmonotoneu : exists b, Proper (R b ==> Z.le) (fun v => upper (f v)))
-        x_bs x
-        (Hboundedx : is_bounded_by_bool x x_bs)
-    : is_tighter_than_bool (f x) (apply_to_range f x_bs).
+  Lemma monotone_n_corners_and_zero_genb
+        n f
+        (Hmonotone : @is_piecewise_monotone_on_projections n f)
+        v v_bs
+        (Hboundedx : @all_are_bounded_by_bool n v v_bs)
+    : is_bounded_by_bool (app f v) (app (n_corners_and_zero f) v_bs).
   Proof.
-    apply (monotone_apply_to_range_genbP (fun _ => True)); cbv [Proper respectful] in *; eauto;
-      destruct_head'_ex;
-      match goal with
-      | [ b : bool |- _ ] => exists b; destruct b; solve [ intuition eauto ]
-      end.
+    destruct n as [|n].
+    { cbv [all_are_bounded_by_bool is_bounded_by_bool is_piecewise_monotone_on_projections is_true] in *; cbn in *.
+      rewrite Bool.andb_true_iff, Z.leb_le; split; reflexivity. }
+    cbv [app tuple all_are_bounded_by_bool fieldwiseb] in *.
+    induction n as [|n IHn].
+    { t_fin_pos. }
+    { destruct v_bs as [ v_bs [l u] ], v as [vs v]; cbn [lower upper] in *.
+      cbn [fieldwiseb' fst snd] in Hboundedx.
+      cbv [is_true] in *.
+      rewrite Bool.andb_true_iff in Hboundedx.
+      destruct Hboundedx as [Hboundedx0 Hboundedx1].
+      destruct Hmonotone as [Hmonotone0 [Hmonotone1 Hmonotone2] ].
+      specialize (fun f pf => IHn f pf vs v_bs Hboundedx0).
+      specialize (fun x => IHn (f x) (Hmonotone0 _)).
+      cbn [app'].
+      set (Sn := S n) in *.
+      cbn [n_corners_and_zero].
+      set (f' := fun x => @n_corners_and_zero Sn (f x)).
+      lazymatch type of IHn with
+      | forall x, is_bounded_by_bool (@?B x) (app' _ ?v_bs) = true
+        => change (forall x, is_bounded_by_bool (B x) (app' (f' x) v_bs) = true) in IHn
+      end; cbv beta in *.
+      clearbody f'.
+      cbn -[Sn] in *.
+      cbv [is_bounded_by_bool app] in *.
+      unfold Sn in Hmonotone1, Hmonotone2.
+      setoid_rewrite Bool.andb_true_iff in IHn.
+      rewrite ?Bool.andb_true_iff in *.
+      setoid_rewrite Z.leb_le in IHn.
+      rewrite !Z.leb_le in *.
+      specialize (Hmonotone1 vs).
+      specialize (Hmonotone2 vs).
+      destruct Hmonotone1 as [? Hmonotone1].
+      destruct Hmonotone2 as [? Hmonotone2].
+      clear -IHn Hboundedx1 Hmonotone1 Hmonotone2.
+      cbn [lower upper] in *.
+      destruct l as [|l|l], u as [|u|u], v as [|v|v].
+      all: try (exfalso; clear -Hboundedx1; lia).
+      all: cbn -[Sn] in *.
+      all: rewrite !pull_union_under_args2.
+      all: cbv [union]; cbn [lower upper].
+      all: repeat match goal with
+                  | [ H : context[Zpos ?p <= Zpos ?q] |- _ ]
+                    => unique assert (Pos.le p q) by lia
+                  | [ H : context[Zneg ?p <= Zneg ?q] |- _ ]
+                    => unique assert (Pos.le q p) by lia
+                  end.
+      all: destruct_head'_bool.
+      all: first [ split; etransitivity;
+                   [ | first [ eapply Hmonotone1 | eapply Hmonotone2 ];
+                       first [ eassumption | eapply Pos.le_1_l ]
+                     | first [ eapply Hmonotone1 | eapply Hmonotone2 ];
+                       first [ eassumption | eapply Pos.le_1_l ] | ]
+                 | split ].
+      all: first [ etransitivity; [ eapply IHn | ] | etransitivity; [ | eapply IHn ] ].
+      all: fast_split_min_max.
+      all: auto using Z.le_refl.
+      all: repeat t_fin_common_step. }
   Qed.
 
+
   Lemma monotone_two_corners_genb'
         (f : Z -> Z)
-        (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
         (Hmonotone : exists b, Proper (R b ==> Z.le) f)
         x_bs x
         (Hboundedx : is_bounded_by_bool x x_bs)
     : is_tighter_than_bool (constant (f x)) (two_corners f x_bs).
   Proof.
-    cbv [two_corners].
-    lazymatch goal with
-    | [ |- context[apply_to_range ?f ?x_bs] ]
-      => apply (monotone_apply_to_range_genb f); auto
-    end.
+    exact (@monotone_n_corners_genb 1 f (ltac:(repeat split; auto)) x x_bs Hboundedx).
   Qed.
 
-  Lemma monotone_two_corners_genb
+  Lemma monotone_two_corners_and_zero_genb'
         (f : Z -> Z)
-        (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
-        (Hmonotone : exists b, Proper (R b ==> Z.le) f)
+        (Hmonotonep : exists b, Proper (Rp b ==> Z.le) (fun x => f (Zpos x)))
+        (Hmonotonen : exists b, Proper (Rp b ==> Z.le) (fun x => f (Zneg x)))
         x_bs x
-        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-    : ZRange.is_bounded_by' None (two_corners f x_bs) (f x).
+        (Hboundedx : is_bounded_by_bool x x_bs)
+    : is_tighter_than_bool (constant (f x)) (two_corners_and_zero f x_bs).
   Proof.
-    pose proof (monotone_two_corners_genb' f Hmonotone x_bs x) as H.
-    cbv [constant is_bounded_by' is_bounded_by_bool is_true is_tighter_than_bool] in *.
-    cbn [upper lower] in *.
-    rewrite ?Bool.andb_true_iff, ?Z.leb_le_iff in *.
-    tauto.
+    unshelve eapply (@monotone_n_corners_and_zero_genb 1 f _ x x_bs Hboundedx).
+    repeat split; auto.
   Qed.
 
-  Lemma monotone_two_corners_gen
+  Lemma monotoneb_two_corners_gen
         (f : Z -> Z)
         (Hmonotone : Proper (Z.le ==> Z.le) f \/ Proper (Basics.flip Z.le ==> Z.le) f)
         x_bs x
-        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-    : ZRange.is_bounded_by' None (ZRange.two_corners f x_bs) (f x).
+        (Hboundedx : ZRange.is_bounded_by_bool x x_bs = true)
+    : ZRange.is_bounded_by_bool (f x) (ZRange.two_corners f x_bs) = true.
   Proof.
-    eapply monotone_two_corners_genb; auto.
-    destruct Hmonotone; [ exists true | exists false ]; assumption.
+    apply (fun pf => monotone_two_corners_genb' f pf _ _ Hboundedx).
+    rewrite Bool.ex_bool_iff_or; auto.
   Qed.
-  Lemma monotone_two_corners
-        (b : bool)
+
+  Lemma monotoneb_two_corners_and_zero_gen
         (f : Z -> Z)
-        (R := if b then Z.le else Basics.flip Z.le)
-        (Hmonotone : Proper (R ==> Z.le) f)
+        (Hmonotonep : Proper (Pos.le ==> Z.le) (fun x => f (Zpos x)) \/ Proper (Basics.flip Pos.le ==> Z.le) (fun x => f (Zpos x)))
+        (Hmonotonen : Proper (Pos.le ==> Z.le) (fun x => f (Zneg x)) \/ Proper (Basics.flip Pos.le ==> Z.le) (fun x => f (Zneg x)))
         x_bs x
-        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-    : ZRange.is_bounded_by' None (ZRange.two_corners f x_bs) (f x).
+        (Hboundedx : ZRange.is_bounded_by_bool x x_bs = true)
+    : ZRange.is_bounded_by_bool (f x) (ZRange.two_corners_and_zero f x_bs) = true.
   Proof.
-    apply monotone_two_corners_genb; auto; subst R;
-      exists b.
-    intros ???; apply Hmonotone; auto.
+    apply (fun pf1 pf2 => monotone_two_corners_and_zero_genb' f pf1 pf2 _ _ Hboundedx).
+    all: rewrite Bool.ex_bool_iff_or; auto.
   Qed.
 
-  (*
+  Local Ltac t_fill :=
+    intros; rewrite ?Bool.ex_bool_iff_or; auto;
+    cbn in *; cbv [is_true] in *; rewrite ?Bool.andb_true_iff; intuition eauto.
+
+  Local Ltac t_red :=
+    cbv [eight_corners_and_zero four_corners_and_zero two_corners_and_zero n_corners_and_zero apply_to_split_range apply_to_split_range_under_args apply_to_each_split_range apply_to_each_split_range_under_args under_args2 apply_to_range apply_to_range_under_args].
+
+  Lemma two_corners_and_zero_eq f x
+    : two_corners_and_zero f x = @n_corners_and_zero 1 f x.
+  Proof. reflexivity. Qed.
+
   Lemma monotone_four_corners_genb'
         (f : Z -> Z -> Z)
-        (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
-        (Hmonotone1 : forall x, exists b, Proper (R b ==> Z.le) (f x))
+        (Hmonotone1 : forall x, exists b, Proper (R b ==> Z.le) (fun y => f x y))
         (Hmonotone2 : forall y, exists b, Proper (R b ==> Z.le) (fun x => f x y))
-        x_bs y_bs x y
+        x x_bs y y_bs
         (Hboundedx : is_bounded_by_bool x x_bs)
         (Hboundedy : is_bounded_by_bool y y_bs)
     : is_tighter_than_bool (constant (f x y)) (four_corners f x_bs y_bs).
   Proof.
-    cbv [four_corners].
-    etransitivity;
-      [ apply monotone_two_corners_genb'; solve [ eauto ]
-      | ].
-    cbv [apply_to_range union two_corners constant is_bounded_by_bool is_tighter_than_bool]; cbn [lower upper] in *.
-      | lazymatch goal with
-        | [ |- context[apply_to_range ?f ?x_bs] ]
-          => apply (monotone_apply_to_range_genb f); [ | | eassumption ]
-        end ];
-      auto.
-    { cbv [two_corners constant apply_to_range union flip].
-      cbn [lower upper].
-      subst R.
-      cbv [is_bounded_by_bool is_true] in *; split_andb; Z.ltb_to_lt.
-      assert (Hx_good : lower x_bs <= upper x_bs) by omega.
-      assert (Hy_good : lower y_bs <= upper y_bs) by omega.
-      pose proof (Hmonotone2 (lower y_bs)).
-      pose proof (Hmonotone2 (upper y_bs)).
-      destruct_head'_ex; destruct_head'_bool; [ exists true | | | exists false ];
-        try intros ?? Hc;
-        repeat match goal with
-               | [ H : Proper _ _ |- _ ] => specialize (H _ _ Hc)
-               end;
-        split_min_max; cbn beta in *; try omega.
-      all: pose proof (Hmonotone1 (lower x_bs)).
-      all: pose proof (Hmonotone1 (upper x_bs)).
-      all: destruct_head'_ex.
-      all: destruct_head'_bool.
-      all: repeat match goal with
-                  | [ H : Proper _ (fun x => ?f x _) |- _ ]
-                    => unique pose proof (H _ _ Hx_good)
-                  | [ H : Proper _ (?f _) |- _ ]
-                    => unique pose proof (H _ _ Hy_good)
-                  end;
-        cbn beta in *.
-      cbv [Basics.flip] in *.
-      all:try omega.
-
-      repeat match goal with
-             | [
-      { exists true.
-
-    cbv [two_corners].
+    apply (fun pf => @monotone_n_corners_genb 2 f pf (y, x) (y_bs, x_bs)).
+    all: t_fill.
+  Qed.
 
-  Qed.*)
+  Lemma four_corners_and_zero_eq f x y
+    : four_corners_and_zero f x y = @n_corners_and_zero 2 f x y.
+  Proof.
+    set (n:=1%nat).
+    cbv [four_corners_and_zero].
+    cbn [n_corners_and_zero].
+    generalize (fun x => two_corners_and_zero_eq (f x)).
+    subst n.
+    generalize (@two_corners_and_zero) (@n_corners_and_zero 1).
+    t_red.
+    break_innermost_match; intros ?? H; rewrite ?H; reflexivity.
+  Qed.
 
-  Lemma monotone_four_corners_genb
+  Lemma monotone_four_corners_and_zero_genb'
         (f : Z -> Z -> Z)
-        (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
-        (Hmonotone1 : forall x, exists b, Proper (R b ==> Z.le) (f x))
-        (Hmonotone2 : forall y, exists b, Proper (R b ==> Z.le) (fun x => f x y))
-        x_bs y_bs x y
-        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-        (Hboundedy : ZRange.is_bounded_by' None y_bs y)
-    : ZRange.is_bounded_by' None (ZRange.four_corners f x_bs y_bs) (f x y).
+        (Hmonotone1p : forall x, exists b, Proper (Rp b ==> Z.le) (fun y => f x (Zpos y)))
+        (Hmonotone1n : forall x, exists b, Proper (Rp b ==> Z.le) (fun y => f x (Zneg y)))
+        (Hmonotone2p : forall y, exists b, Proper (Rp b ==> Z.le) (fun x => f (Zpos x) y))
+        (Hmonotone2n : forall y, exists b, Proper (Rp b ==> Z.le) (fun x => f (Zneg x) y))
+        x x_bs y y_bs
+        (Hboundedx : is_bounded_by_bool x x_bs)
+        (Hboundedy : is_bounded_by_bool y y_bs)
+    : is_tighter_than_bool (constant (f x y)) (four_corners_and_zero f x_bs y_bs).
   Proof.
-    destruct x_bs as [lx ux].
-    cbn [ZRange.four_corners lower upper].
-    pose proof (monotone_two_corners_genb (f lx) (Hmonotone1 _) _ _ Hboundedy) as Hmono_fl.
-    pose proof (monotone_two_corners_genb (f ux) (Hmonotone1 _) _ _ Hboundedy) as Hmono_fu.
-    repeat match goal with
-           | [ |- context[ZRange.two_corners ?x ?y] ]
-             => let l := fresh "lf" in
-                let u := fresh "uf" in
-                generalize dependent (ZRange.two_corners x y); intros [l u]; intros
-           end.
-    unfold ZRange.is_bounded_by', union in *; simpl in *; split; trivial.
-    destruct_head'_and; destruct_head' True.
-    pose proof (Hmonotone2 y).
-    destruct_head'_ex.
-    repeat match goal with
-           | [ H : Proper (R ?b ==> Z.le) (f _) |- _ ]
-             => unique assert (R b (if b then ly else y) (if b then y else ly)
-                               /\ R b (if b then y else uy) (if b then uy else y))
-               by (unfold R, Basics.flip; destruct b; omega)
-           | [ H : Proper (R ?b ==> Z.le) (fun x => f x _) |- _ ]
-             => unique assert (R b (if b then lx else x) (if b then x else lx)
-                               /\ R b (if b then x else ux) (if b then ux else x))
-               by (unfold R, Basics.flip; destruct b; omega)
-           end.
-    destruct_head' and.
-    repeat match goal with
-           | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ]
-             => unique pose proof (H _ _ H')
-           end; cbv beta in *.
-    destruct_head bool.
-    all: revert_min_max; intros.
-    all: (split; [ repeat (etransitivity; [ | eassumption ]) | repeat (etransitivity; [ eassumption | ]) ]).
-    all: auto using Z.le_min_l, Z.le_min_r, Z.le_max_l, Z.le_max_r.
+    rewrite four_corners_and_zero_eq.
+    exact (@monotone_n_corners_and_zero_genb 2 f ltac:(t_fill) (y, x) (y_bs, x_bs) ltac:(t_fill)).
   Qed.
 
-  Lemma monotone_four_corners_gen
+  Lemma monotoneb_four_corners_gen
         (f : Z -> Z -> Z)
-        (Hmonotone1 : forall x, Proper (Z.le ==> Z.le) (f x) \/ Proper (Basics.flip Z.le ==> Z.le) (f x))
-        (Hmonotone2 : forall y, Proper (Z.le ==> Z.le) (fun x => f x y) \/ Proper (Basics.flip Z.le ==> Z.le) (fun x => f x y))
-        x_bs y_bs x y
-        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-        (Hboundedy : ZRange.is_bounded_by' None y_bs y)
-    : ZRange.is_bounded_by' None (ZRange.four_corners f x_bs y_bs) (f x y).
+        (Hmonotone1 : forall x, Proper (R true ==> Z.le) (fun y => f x y) \/ Proper (R false ==> Z.le) (fun y => f x y))
+        (Hmonotone2 : forall y, Proper (R true ==> Z.le) (fun x => f x y) \/ Proper (R false ==> Z.le) (fun x => f x y))
+        x x_bs y y_bs
+        (Hboundedx : is_bounded_by_bool x x_bs)
+        (Hboundedy : is_bounded_by_bool y y_bs)
+    : is_tighter_than_bool (constant (f x y)) (four_corners f x_bs y_bs).
   Proof.
-    eapply monotone_four_corners_genb; auto.
-    { intro x'; destruct (Hmonotone1 x'); [ exists true | exists false ]; assumption. }
-    { intro x'; destruct (Hmonotone2 x'); [ exists true | exists false ]; assumption. }
+    apply monotone_four_corners_genb'; t_fill.
   Qed.
-  Lemma monotone_four_corners
-        (b1 b2 : bool)
+
+  Lemma monotoneb_four_corners_and_zero_gen
         (f : Z -> Z -> Z)
-        (R1 := if b1 then Z.le else Basics.flip Z.le) (R2 := if b2 then Z.le else Basics.flip Z.le)
-        (Hmonotone : Proper (R1 ==> R2 ==> Z.le) f)
-        x_bs y_bs x y
-        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-        (Hboundedy : ZRange.is_bounded_by' None y_bs y)
-    : ZRange.is_bounded_by' None (ZRange.four_corners f x_bs y_bs) (f x y).
+        (Hmonotone1p : forall x, Proper (Rp true ==> Z.le) (fun y => f x (Zpos y)) \/ Proper (Rp false ==> Z.le) (fun y => f x (Zpos y)))
+        (Hmonotone1n : forall x, Proper (Rp true ==> Z.le) (fun y => f x (Zneg y)) \/ Proper (Rp false ==> Z.le) (fun y => f x (Zneg y)))
+        (Hmonotone2p : forall y, Proper (Rp true ==> Z.le) (fun x => f (Zpos x) y) \/ Proper (Rp false ==> Z.le) (fun x => f (Zpos x) y))
+        (Hmonotone2n : forall y, Proper (Rp true ==> Z.le) (fun x => f (Zneg x) y) \/ Proper (Rp false ==> Z.le) (fun x => f (Zneg x) y))
+        x x_bs y y_bs
+        (Hboundedx : is_bounded_by_bool x x_bs)
+        (Hboundedy : is_bounded_by_bool y y_bs)
+    : is_tighter_than_bool (constant (f x y)) (four_corners_and_zero f x_bs y_bs).
   Proof.
-    apply monotone_four_corners_genb; auto; intro x'; subst R1 R2;
-      [ exists b2 | exists b1 ];
-      [ eapply (Hmonotone x' x'); destruct b1; reflexivity
-      | intros ???; apply Hmonotone; auto; destruct b2; reflexivity ].
+    apply monotone_four_corners_and_zero_genb'; t_fill.
   Qed.
 
-  Lemma monotone_eight_corners_genb
+
+  Lemma monotone_eight_corners_genb'
         (f : Z -> Z -> Z -> Z)
-        (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
-        (Hmonotone1 : forall x y, exists b, Proper (R b ==> Z.le) (f x y))
+        (Hmonotone1 : forall x y, exists b, Proper (R b ==> Z.le) (fun z => f x y z))
         (Hmonotone2 : forall x z, exists b, Proper (R b ==> Z.le) (fun y => f x y z))
         (Hmonotone3 : forall y z, exists b, Proper (R b ==> Z.le) (fun x => f x y z))
-        x_bs y_bs z_bs x y z
-        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-        (Hboundedy : ZRange.is_bounded_by' None y_bs y)
-        (Hboundedz : ZRange.is_bounded_by' None z_bs z)
-    : ZRange.is_bounded_by' None (ZRange.eight_corners f x_bs y_bs z_bs) (f x y z).
+        x x_bs y y_bs z z_bs
+        (Hboundedx : is_bounded_by_bool x x_bs)
+        (Hboundedy : is_bounded_by_bool y y_bs)
+        (Hboundedz : is_bounded_by_bool z z_bs)
+    : is_tighter_than_bool (constant (f x y z)) (eight_corners f x_bs y_bs z_bs).
+  Proof.
+    apply (fun pf => @monotone_n_corners_genb 3 f pf (z, y, x) (z_bs, y_bs, x_bs)).
+    all: t_fill.
+  Qed.
+
+  Lemma eight_corners_and_zero_eq f x y z
+    : eight_corners_and_zero f x y z = @n_corners_and_zero 3 f x y z.
   Proof.
-    destruct x_bs as [lx ux].
-    unfold ZRange.eight_corners; cbn [lower upper].
-    pose proof (monotone_four_corners_genb (f lx) (Hmonotone1 _) (Hmonotone2 _) _ _ _ _ Hboundedy Hboundedz) as Hmono_fl.
-    pose proof (monotone_four_corners_genb (f ux) (Hmonotone1 _) (Hmonotone2 _) _ _ _ _ Hboundedy Hboundedz) as Hmono_fu.
-    repeat match goal with
-           | [ |- context[ZRange.four_corners ?x ?y ?z] ]
-             => let l := fresh "lf" in
-                let u := fresh "uf" in
-                generalize dependent (ZRange.four_corners x y z); intros [l u]; intros
-           end.
-    unfold ZRange.is_bounded_by' in *; simpl in *; split; trivial.
-    destruct_head'_and; destruct_head' True.
-    pose proof (Hmonotone3 y z).
-    destruct_head'_ex.
-    repeat match goal with
-           | [ H : Proper (R ?b ==> Z.le) (f _ _) |- _ ]
-             => unique assert (R b (if b then lz else z) (if b then z else lz)
-                               /\ R b (if b then z else uz) (if b then uz else z))
-               by (unfold R, Basics.flip; destruct b; omega)
-           | [ H : Proper (R ?b ==> Z.le) (fun y' => f _ y' _) |- _ ]
-             => unique assert (R b (if b then ly else y) (if b then y else ly)
-                               /\ R b (if b then y else uy) (if b then uy else y))
-               by (unfold R, Basics.flip; destruct b; omega)
-           | [ H : Proper (R ?b ==> Z.le) (fun x' => f x' _ _) |- _ ]
-             => unique assert (R b (if b then lx else x) (if b then x else lx)
-                               /\ R b (if b then x else ux) (if b then ux else x))
-               by (unfold R, Basics.flip; destruct b; omega)
-           end.
-    destruct_head' and.
-    repeat match goal with
-           | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ]
-             => unique pose proof (H _ _ H')
-           end.
-    destruct_head bool.
-    all: revert_min_max; intros.
-    all: (split; [ repeat (etransitivity; [ | eassumption ]) | repeat (etransitivity; [ eassumption | ]) ]).
-    all: auto using Z.le_min_l, Z.le_min_r, Z.le_max_l, Z.le_max_r.
+    set (n:=2%nat).
+    cbv [eight_corners_and_zero].
+    cbn [n_corners_and_zero].
+    generalize (fun x => four_corners_and_zero_eq (f x)).
+    subst n.
+    generalize (@four_corners_and_zero) (@n_corners_and_zero 2).
+    t_red.
+    break_innermost_match; intros ?? H; rewrite ?H; reflexivity.
   Qed.
-  Lemma monotone_eight_corners
-        (b1 b2 b3 : bool)
+
+  Lemma monotone_eight_corners_and_zero_genb'
         (f : Z -> Z -> Z -> Z)
-        (R1 := if b1 then Z.le else Basics.flip Z.le)
-        (R2 := if b2 then Z.le else Basics.flip Z.le)
-        (R3 := if b3 then Z.le else Basics.flip Z.le)
-        (Hmonotone : Proper (R1 ==> R2 ==> R3 ==> Z.le) f)
-        x_bs y_bs z_bs x y z
-        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-        (Hboundedy : ZRange.is_bounded_by' None y_bs y)
-        (Hboundedz : ZRange.is_bounded_by' None z_bs z)
-    : ZRange.is_bounded_by' None (ZRange.eight_corners f x_bs y_bs z_bs) (f x y z).
+        (Hmonotone1p : forall x y, exists b, Proper (Rp b ==> Z.le) (fun z => f x y (Zpos z)))
+        (Hmonotone1n : forall x y, exists b, Proper (Rp b ==> Z.le) (fun z => f x y (Zneg z)))
+        (Hmonotone2p : forall x z, exists b, Proper (Rp b ==> Z.le) (fun y => f x (Zpos y) z))
+        (Hmonotone2n : forall x z, exists b, Proper (Rp b ==> Z.le) (fun y => f x (Zneg y) z))
+        (Hmonotone3p : forall y z, exists b, Proper (Rp b ==> Z.le) (fun x => f (Zpos x) y z))
+        (Hmonotone3n : forall y z, exists b, Proper (Rp b ==> Z.le) (fun x => f (Zneg x) y z))
+        x x_bs y y_bs z z_bs
+        (Hboundedx : is_bounded_by_bool x x_bs)
+        (Hboundedy : is_bounded_by_bool y y_bs)
+        (Hboundedz : is_bounded_by_bool z z_bs)
+    : is_tighter_than_bool (constant (f x y z)) (eight_corners_and_zero f x_bs y_bs z_bs).
   Proof.
-    apply monotone_eight_corners_genb; auto; intro x'; subst R1 R2 R3;
-      [ exists b3 | exists b2 | exists b1 ];
-      intros ???; apply Hmonotone; break_innermost_match; try reflexivity; trivial.
+    rewrite eight_corners_and_zero_eq.
+    exact (@monotone_n_corners_and_zero_genb 3 f ltac:(t_fill) (z, y, x) (z_bs, y_bs, x_bs) ltac:(t_fill)).
   Qed.
 
-  Lemma monotonify2 (f : Z -> Z -> Z) (upper : Z -> Z -> Z)
-        (Hbounded : forall a b, Z.abs (f a b) <= upper (Z.abs a) (Z.abs b))
-        (Hupper_monotone : Proper (Z.le ==> Z.le ==> Z.le) upper)
-        {xb yb x y}
-        (Hboundedx : ZRange.is_bounded_by' None xb x)
-        (Hboundedy : ZRange.is_bounded_by' None yb y)
-        (abs_x := ZRange.upper (ZRange.abs xb))
-        (abs_y := ZRange.upper (ZRange.abs yb))
-    : ZRange.is_bounded_by'
-        None
-        {| ZRange.lower := -upper abs_x abs_y;
-           ZRange.upper := upper abs_x abs_y |}
-        (f x y).
+  Lemma monotoneb_eight_corners_gen
+        (f : Z -> Z -> Z -> Z)
+        (Hmonotone1 : forall x y, Proper (R true ==> Z.le) (fun z => f x y z) \/ Proper (R false ==> Z.le) (fun z => f x y z))
+        (Hmonotone2 : forall x z, Proper (R true ==> Z.le) (fun y => f x y z) \/ Proper (R false ==> Z.le) (fun y => f x y z))
+        (Hmonotone3 : forall y z, Proper (R true ==> Z.le) (fun x => f x y z) \/ Proper (R false ==> Z.le) (fun x => f x y z))
+        x x_bs y y_bs z z_bs
+        (Hboundedx : is_bounded_by_bool x x_bs)
+        (Hboundedy : is_bounded_by_bool y y_bs)
+        (Hboundedz : is_bounded_by_bool z z_bs)
+    : is_tighter_than_bool (constant (f x y z)) (eight_corners f x_bs y_bs z_bs).
   Proof.
-    split; [ | exact I ]; subst abs_x abs_y; simpl.
-    apply Z.abs_le.
-    destruct Hboundedx as [Hx _], Hboundedy as [Hy _].
-    etransitivity; [ apply Hbounded | ].
-    apply Hupper_monotone;
-      unfold ZRange.abs;
-      repeat (apply Z.max_case_strong || apply Zabs_ind); omega.
+    apply monotone_eight_corners_genb'; t_fill.
   Qed.
+
+  Lemma monotoneb_eight_corners_and_zero_gen
+        (f : Z -> Z -> Z -> Z)
+        (Hmonotone1p : forall x y, Proper (Rp true ==> Z.le) (fun z => f x y (Zpos z)) \/ Proper (Rp false ==> Z.le) (fun z => f x y (Zpos z)))
+        (Hmonotone1n : forall x y, Proper (Rp true ==> Z.le) (fun z => f x y (Zneg z)) \/ Proper (Rp false ==> Z.le) (fun z => f x y (Zneg z)))
+        (Hmonotone2p : forall x z, Proper (Rp true ==> Z.le) (fun y => f x (Zpos y) z) \/ Proper (Rp false ==> Z.le) (fun y => f x (Zpos y) z))
+        (Hmonotone2n : forall x z, Proper (Rp true ==> Z.le) (fun y => f x (Zneg y) z) \/ Proper (Rp false ==> Z.le) (fun y => f x (Zneg y) z))
+        (Hmonotone3p : forall y z, Proper (Rp true ==> Z.le) (fun x => f (Zpos x) y z) \/ Proper (Rp false ==> Z.le) (fun x => f (Zpos x) y z))
+        (Hmonotone3n : forall y z, Proper (Rp true ==> Z.le) (fun x => f (Zneg x) y z) \/ Proper (Rp false ==> Z.le) (fun x => f (Zneg x) y z))
+        x x_bs y y_bs z z_bs
+        (Hboundedx : is_bounded_by_bool x x_bs)
+        (Hboundedy : is_bounded_by_bool y y_bs)
+        (Hboundedz : is_bounded_by_bool z z_bs)
+    : is_tighter_than_bool (constant (f x y z)) (eight_corners_and_zero f x_bs y_bs z_bs).
+  Proof.
+    apply monotone_eight_corners_and_zero_genb'; t_fill.
+  Qed.
+
+  Section legacy.
+    (** TODO: When we move to the new pipeline, remove this *)
+    Lemma monotone_two_corners_genb
+          (f : Z -> Z)
+          (Hmonotone : exists b, Proper (R b ==> Z.le) f)
+          x_bs x
+          (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+    : ZRange.is_bounded_by' None (two_corners f x_bs) (f x).
+    Proof.
+      pose proof (monotone_two_corners_genb' f Hmonotone x_bs x) as H.
+      cbv [constant is_bounded_by' is_bounded_by_bool is_true is_tighter_than_bool] in *.
+      cbn [upper lower] in *.
+      rewrite ?Bool.andb_true_iff, ?Z.leb_le_iff in *.
+      tauto.
+    Qed.
+
+    Lemma monotone_two_corners_gen
+          (f : Z -> Z)
+          (Hmonotone : Proper (Z.le ==> Z.le) f \/ Proper (Basics.flip Z.le ==> Z.le) f)
+          x_bs x
+          (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+      : ZRange.is_bounded_by' None (ZRange.two_corners f x_bs) (f x).
+    Proof.
+      eapply monotone_two_corners_genb; auto.
+      destruct Hmonotone; [ exists true | exists false ]; assumption.
+    Qed.
+
+    Lemma monotone_two_corners
+          (b : bool)
+          (f : Z -> Z)
+          (Hmonotone : Proper (R b ==> Z.le) f)
+          x_bs x
+          (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+      : ZRange.is_bounded_by' None (ZRange.two_corners f x_bs) (f x).
+    Proof.
+      apply monotone_two_corners_genb; auto;
+        exists b.
+      intros ???; apply Hmonotone; auto.
+    Qed.
+
+    Lemma monotone_four_corners_genb
+          (f : Z -> Z -> Z)
+          (Hmonotone1 : forall x, exists b, Proper (R b ==> Z.le) (f x))
+          (Hmonotone2 : forall y, exists b, Proper (R b ==> Z.le) (fun x => f x y))
+          x_bs y_bs x y
+          (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+          (Hboundedy : ZRange.is_bounded_by' None y_bs y)
+      : ZRange.is_bounded_by' None (ZRange.four_corners f x_bs y_bs) (f x y).
+    Proof.
+      destruct x_bs as [lx ux].
+      pose proof (monotone_two_corners_genb (f lx) (Hmonotone1 _) _ _ Hboundedy) as Hmono_fl.
+      pose proof (monotone_two_corners_genb (f ux) (Hmonotone1 _) _ _ Hboundedy) as Hmono_fu.
+      unfold ZRange.is_bounded_by', union in *; simpl in *; split; trivial.
+      destruct_head'_and; destruct_head' True.
+      pose proof (Hmonotone2 y).
+      destruct_head'_ex.
+      repeat match goal with
+             | [ H : Proper (R ?b ==> Z.le) (f _) |- _ ]
+               => unique assert (R b (if b then ly else y) (if b then y else ly)
+                                 /\ R b (if b then y else uy) (if b then uy else y))
+                 by (unfold Basics.flip; destruct b; omega)
+             | [ H : Proper (R ?b ==> Z.le) (fun x => f x _) |- _ ]
+               => unique assert (R b (if b then lx else x) (if b then x else lx)
+                                 /\ R b (if b then x else ux) (if b then ux else x))
+                 by (unfold Basics.flip; destruct b; omega)
+             end.
+      destruct_head' and.
+      repeat match goal with
+             | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ]
+               => unique pose proof (H _ _ H')
+             end; cbv beta in *.
+      destruct_head bool.
+      all: revert_min_max; intros.
+      all: (split; [ repeat (etransitivity; [ | eassumption ]) | repeat (etransitivity; [ eassumption | ]) ]).
+      all: auto using Z.le_min_l, Z.le_min_r, Z.le_max_l, Z.le_max_r.
+    Qed.
+
+    Lemma monotone_four_corners_gen
+          (f : Z -> Z -> Z)
+          (Hmonotone1 : forall x, Proper (Z.le ==> Z.le) (f x) \/ Proper (Basics.flip Z.le ==> Z.le) (f x))
+          (Hmonotone2 : forall y, Proper (Z.le ==> Z.le) (fun x => f x y) \/ Proper (Basics.flip Z.le ==> Z.le) (fun x => f x y))
+          x_bs y_bs x y
+          (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+          (Hboundedy : ZRange.is_bounded_by' None y_bs y)
+      : ZRange.is_bounded_by' None (ZRange.four_corners f x_bs y_bs) (f x y).
+    Proof.
+      eapply monotone_four_corners_genb; auto.
+      { intro x'; destruct (Hmonotone1 x'); [ exists true | exists false ]; assumption. }
+      { intro x'; destruct (Hmonotone2 x'); [ exists true | exists false ]; assumption. }
+    Qed.
+    Lemma monotone_four_corners
+          (b1 b2 : bool)
+          (f : Z -> Z -> Z)
+          (R1 := if b1 then Z.le else Basics.flip Z.le) (R2 := if b2 then Z.le else Basics.flip Z.le)
+          (Hmonotone : Proper (R1 ==> R2 ==> Z.le) f)
+          x_bs y_bs x y
+          (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+          (Hboundedy : ZRange.is_bounded_by' None y_bs y)
+      : ZRange.is_bounded_by' None (ZRange.four_corners f x_bs y_bs) (f x y).
+    Proof.
+      apply monotone_four_corners_genb; auto; intro x'; subst R1 R2;
+        [ exists b2 | exists b1 ];
+        [ eapply (Hmonotone x' x'); destruct b1; reflexivity
+        | intros ???; apply Hmonotone; auto; destruct b2; reflexivity ].
+    Qed.
+
+    Lemma monotone_eight_corners_genb
+          (f : Z -> Z -> Z -> Z)
+          (Hmonotone1 : forall x y, exists b, Proper (R b ==> Z.le) (f x y))
+          (Hmonotone2 : forall x z, exists b, Proper (R b ==> Z.le) (fun y => f x y z))
+          (Hmonotone3 : forall y z, exists b, Proper (R b ==> Z.le) (fun x => f x y z))
+          x_bs y_bs z_bs x y z
+          (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+          (Hboundedy : ZRange.is_bounded_by' None y_bs y)
+          (Hboundedz : ZRange.is_bounded_by' None z_bs z)
+      : ZRange.is_bounded_by' None (ZRange.eight_corners f x_bs y_bs z_bs) (f x y z).
+    Proof.
+      destruct x_bs as [lx ux].
+      unfold ZRange.eight_corners; cbn [lower upper].
+      pose proof (monotone_four_corners_genb (f lx) (Hmonotone1 _) (Hmonotone2 _) _ _ _ _ Hboundedy Hboundedz) as Hmono_fl.
+      pose proof (monotone_four_corners_genb (f ux) (Hmonotone1 _) (Hmonotone2 _) _ _ _ _ Hboundedy Hboundedz) as Hmono_fu.
+      repeat match goal with
+             | [ |- context[ZRange.four_corners ?x ?y ?z] ]
+               => let l := fresh "lf" in
+                  let u := fresh "uf" in
+                  generalize dependent (ZRange.four_corners x y z); intros [l u]; intros
+             end.
+      unfold ZRange.is_bounded_by' in *; simpl in *; split; trivial.
+      destruct_head'_and; destruct_head' True.
+      pose proof (Hmonotone3 y z).
+      destruct_head'_ex.
+      repeat match goal with
+             | [ H : Proper (R ?b ==> Z.le) (f _ _) |- _ ]
+               => unique assert (R b (if b then lz else z) (if b then z else lz)
+                                 /\ R b (if b then z else uz) (if b then uz else z))
+                 by (unfold Basics.flip; destruct b; omega)
+             | [ H : Proper (R ?b ==> Z.le) (fun y' => f _ y' _) |- _ ]
+               => unique assert (R b (if b then ly else y) (if b then y else ly)
+                                 /\ R b (if b then y else uy) (if b then uy else y))
+                 by (unfold Basics.flip; destruct b; omega)
+             | [ H : Proper (R ?b ==> Z.le) (fun x' => f x' _ _) |- _ ]
+               => unique assert (R b (if b then lx else x) (if b then x else lx)
+                                 /\ R b (if b then x else ux) (if b then ux else x))
+                 by (unfold Basics.flip; destruct b; omega)
+             end.
+      destruct_head' and.
+      repeat match goal with
+             | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ]
+               => unique pose proof (H _ _ H')
+             end.
+      destruct_head bool.
+      all: revert_min_max; intros.
+      all: (split; [ repeat (etransitivity; [ | eassumption ]) | repeat (etransitivity; [ eassumption | ]) ]).
+      all: auto using Z.le_min_l, Z.le_min_r, Z.le_max_l, Z.le_max_r.
+    Qed.
+    Lemma monotone_eight_corners
+          (b1 b2 b3 : bool)
+          (f : Z -> Z -> Z -> Z)
+          (R1 := if b1 then Z.le else Basics.flip Z.le)
+          (R2 := if b2 then Z.le else Basics.flip Z.le)
+          (R3 := if b3 then Z.le else Basics.flip Z.le)
+          (Hmonotone : Proper (R1 ==> R2 ==> R3 ==> Z.le) f)
+          x_bs y_bs z_bs x y z
+          (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+          (Hboundedy : ZRange.is_bounded_by' None y_bs y)
+          (Hboundedz : ZRange.is_bounded_by' None z_bs z)
+      : ZRange.is_bounded_by' None (ZRange.eight_corners f x_bs y_bs z_bs) (f x y z).
+    Proof.
+      apply monotone_eight_corners_genb; auto; intro x'; subst R1 R2 R3;
+        [ exists b3 | exists b2 | exists b1 ];
+        intros ???; apply Hmonotone; break_innermost_match; try reflexivity; trivial.
+    Qed.
+
+    Lemma monotonify2 (f : Z -> Z -> Z) (upper : Z -> Z -> Z)
+          (Hbounded : forall a b, Z.abs (f a b) <= upper (Z.abs a) (Z.abs b))
+          (Hupper_monotone : Proper (Z.le ==> Z.le ==> Z.le) upper)
+          {xb yb x y}
+          (Hboundedx : ZRange.is_bounded_by' None xb x)
+          (Hboundedy : ZRange.is_bounded_by' None yb y)
+          (abs_x := ZRange.upper (ZRange.abs xb))
+          (abs_y := ZRange.upper (ZRange.abs yb))
+      : ZRange.is_bounded_by'
+          None
+          {| ZRange.lower := -upper abs_x abs_y;
+             ZRange.upper := upper abs_x abs_y |}
+          (f x y).
+    Proof.
+      split; [ | exact I ]; subst abs_x abs_y; simpl.
+      apply Z.abs_le.
+      destruct Hboundedx as [Hx _], Hboundedy as [Hy _].
+      etransitivity; [ apply Hbounded | ].
+      apply Hupper_monotone;
+        unfold ZRange.abs;
+        repeat (apply Z.max_case_strong || apply Zabs_ind); omega.
+    Qed.
+  End legacy.
 End ZRange.
diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v
index 32af62ee5..c8db4adf0 100644
--- a/src/Util/ZRange/Operations.v
+++ b/src/Util/ZRange/Operations.v
@@ -72,6 +72,55 @@ Module ZRange.
 
   Definition constant (v : Z) : zrange := r[v ~> v].
 
+  Fixpoint nary_T (A B : Type) (n : nat) :=
+    match n with
+    | O => B
+    | S n => A -> nary_T A B n
+    end.
+
+  Fixpoint under_args {A B B'} (F : B -> B') {n : nat} : nary_T A B n -> nary_T A B' n
+    := match n with
+       | O => F
+       | S n => fun f x => @under_args A B B' F n (f x)
+       end.
+
+  Fixpoint under_args2 {A B B' B''} (F : B -> B' -> B'') {n : nat} : nary_T A B n -> nary_T A B' n -> nary_T A B'' n
+    := match n with
+       | O => F
+       | S n => fun f g x => @under_args2 A B B' B'' F n (f x) (g x)
+       end.
+
+  Definition apply_to_range_under_args {A} {n} (f : Z -> nary_T A zrange n) (v : zrange) : nary_T A zrange n
+    := let (l, u) := eta v in
+       under_args2 union (f l) (f u).
+
+  Definition apply_to_split_range_under_args {A} {n} (f : zrange -> nary_T A zrange n) (v : zrange) : nary_T A zrange n
+    := match split_range_at_0 v with
+       | (Some n, Some z, Some p) => under_args2 union (under_args2 union (f n) (f p)) (f z)
+       | (Some v1, Some v2, None) | (Some v1, None, Some v2) | (None, Some v1, Some v2) => under_args2 union (f v1) (f v2)
+       | (Some v, None, None) | (None, Some v, None) | (None, None, Some v) => f v
+       | (None, None, None) => f v
+       end.
+
+  Definition apply_to_each_split_range_under_args {A} {n} (f : BinInt.Z -> nary_T A zrange n) (v : zrange) : nary_T A zrange n
+    := apply_to_split_range_under_args (apply_to_range_under_args f) v.
+
+  Fixpoint n_corners {n : nat} : nary_T Z Z n -> nary_T zrange zrange n
+    := match n with
+       | O => constant
+       | S n
+         => fun (f : Z -> nary_T Z Z n) (v : zrange)
+            => apply_to_range_under_args (fun x => n_corners (f x)) v
+       end.
+
+  Fixpoint n_corners_and_zero {n : nat} : nary_T Z Z n -> nary_T zrange zrange n
+    := match n with
+       | O => constant
+       | S n
+         => fun (f : Z -> nary_T Z Z n) (v : zrange)
+            => apply_to_each_split_range_under_args (fun x => n_corners_and_zero (f x)) v
+       end.
+
   Definition two_corners (f : Z -> Z) (v : zrange) : zrange
     := apply_to_range (fun x => constant (f x)) v.
   Definition four_corners (f : Z -> Z -> Z) (x y : zrange) : zrange