diff --git a/src/AbstractInterpretation/ZRange.v b/src/AbstractInterpretation/ZRange.v
index 200ede3e75..7e61de8c8e 100644
--- a/src/AbstractInterpretation/ZRange.v
+++ b/src/AbstractInterpretation/ZRange.v
@@ -282,6 +282,29 @@ Module Compilers.
           Lemma interp_beq_lb {t x y} : x = y -> @interp_beq t t x y = true.
           Proof. apply reflect_to_beq; exact _. Qed.
 
+          Fixpoint union {t} : interp t -> interp t -> interp t
+            := match t return interp t -> interp t -> interp t with
+               | base.type.type_base base.type.Z => Option.map2 ZRange.union
+               | base.type.type_base _ as t
+               | base.type.unit as t
+                 => fun x y
+                    => if @interp_beq t t x y
+                       then x
+                       else None
+               | base.type.prod A B => fun '(a, b) '(a', b') =>
+                 (@union A a a', @union B b b')
+               | base.type.list A => fun la lb => Option.bind2 la lb (fun la lb =>
+                 if Nat.eqb (length la) (length lb)
+                 then Datatypes.Some (List.map (uncurry (@union A)) (List.combine la lb))
+                 else Datatypes.None)
+               | base.type.option A => fun oa ob => Option.bind2 oa ob (fun l r =>
+                 match l, r return option (option (interp A)) with
+                 | Datatypes.Some l, Datatypes.Some r => Datatypes.Some (Datatypes.Some (union l r))
+                 | Datatypes.None, Datatypes.None => Datatypes.Some Datatypes.None
+                 | _, _ => Datatypes.None
+                 end)
+               end.
+
           Fixpoint is_bounded_by {t} : interp t -> binterp t -> bool
             := match t with
                | base.type.type_base base.type.Z as t
@@ -573,12 +596,6 @@ Module Compilers.
                      | None => None
                      end
              | ident.Z_eqb as idc
-             | ident.Z_leb as idc
-             | ident.Z_ltb as idc
-             | ident.Z_geb as idc
-             | ident.Z_gtb as idc
-             | ident.Z_max as idc
-             | ident.Z_min as idc
              | ident.Z_pow as idc
              | ident.Z_lxor as idc
              | ident.Z_modulo as idc
@@ -623,13 +640,13 @@ Module Compilers.
                => fun t f b
                  => match b with
                    | Some b => if b then t tt else f tt
-                   | None => ZRange.type.base.option.None
+                   | None => type.base.option.union (t tt) (f tt)
                    end
              | ident.bool_rect_nodep _
                => fun t f b
                  => match b with
                    | Some b => if b then t else f
-                   | None => ZRange.type.base.option.None
+                   | None => type.base.option.union t f
                    end
              | ident.option_rect _ _
                => fun s n o
@@ -737,10 +754,17 @@ Module Compilers.
              | ident.List_app _
                => fun ls1 ls2 => ls1 <- ls1; ls2 <- ls2; Some (List.app ls1 ls2)
              | ident.List_rev _ => option_map (@List.rev _)
+             | ident.Z_leb as idc
+             | ident.Z_ltb as idc
+             | ident.Z_geb as idc
+             | ident.Z_gtb as idc
+               => fun x y => x <- x; y <- y; ZRange.ToConstant.four_corners Bool.eqb (ident.interp idc) x y
              | ident.Z_opp as idc
              | ident.Z_log2 as idc
              | ident.Z_log2_up as idc
                => fun x => x <- x; Some (ZRange.two_corners (ident.interp idc) x)
+             | ident.Z_max as idc
+             | ident.Z_min as idc
              | ident.Z_add as idc
              | ident.Z_mul as idc
              | ident.Z_sub as idc
diff --git a/src/AbstractInterpretation/ZRangeProofs.v b/src/AbstractInterpretation/ZRangeProofs.v
index f09333f70a..aad9dd774c 100644
--- a/src/AbstractInterpretation/ZRangeProofs.v
+++ b/src/AbstractInterpretation/ZRangeProofs.v
@@ -41,6 +41,7 @@ Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Tactics.SpecializeAllWays.
 Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Util.Tactics.PrintGoal.
+Require Import Crypto.Util.Tactics.DoWithHyp.
 Require Import Crypto.Language.PreExtra.
 Require Import Crypto.CastLemmas.
 Require Import Crypto.AbstractInterpretation.ZRange.
@@ -58,6 +59,61 @@ Module Compilers.
         Module option.
           Lemma is_bounded_by_None t v : ZRange.type.base.option.is_bounded_by (@ZRange.type.base.option.None t) v = true.
           Proof. induction t; cbn; cbv [andb]; break_innermost_match; eauto. Qed.
+
+          Lemma tighter_than_union t (rx ry : ZRange.type.base.option.interp t) :
+            ZRange.type.base.option.is_tighter_than rx (ZRange.type.base.option.union rx ry) = true /\
+              ZRange.type.base.option.is_tighter_than ry (ZRange.type.base.option.union rx ry) = true.
+          Proof.
+            induction t; [destruct t|..]; destruct rx, ry;
+              cbn [
+                  ZRange.type.base.interp
+                    ZRange.type.base.option.interp
+                    ZRange.type.base.option.is_tighter_than
+                    ZRange.type.base.is_tighter_than
+                    ZRange.type.base.option.union
+                    Option.map2
+                    Option.bind2
+                ] in *; auto 2.
+            all: fold (@ZRange.type.base.option.interp) in *.
+            all: break_innermost_match; reflect_hyps; inversion_option; subst; auto 2.
+            all: split_and.
+            all: cbn [option_beq].
+            all: rewrite ?Bool.andb_true_iff; auto.
+            all: try now split; first [ apply ZRange.is_tighter_than_bool_union_l | apply ZRange.is_tighter_than_bool_union_r ].
+            all: do 2 try (match goal with
+                           | [ |- context[?x = true] ]
+                             => lazymatch x with true => fail | false => fail | _ => idtac end;
+                                destruct x eqn:?; progress reflect_hyps
+                           end;
+                           cbn [ZRange.type.base.option.None] in *;
+                           auto 2; subst; try congruence).
+            { rewrite 2 fold_andb_map_map.
+              rewrite 2 fold_andb_map_iff.
+              rewrite List.combine_length.
+              do_with_hyp' ltac:(fun H => rewrite H).
+              rewrite Nat.min_id.
+              repeat split; intros *; destruct_head'_prod; cbn [uncurry fst snd].
+              all: rewrite In_nth_error_iff.
+              all: intros [n H']; revert H'.
+              all: rewrite !nth_error_combine.
+              all: break_innermost_match; intros; inversion_option; inversion_pair; subst; auto. }
+          Qed.
+
+          Lemma is_bounded_by_union_l t (rx ry : ZRange.type.base.option.interp t) x :
+            ZRange.type.base.option.is_bounded_by rx x = true ->
+            ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union rx ry) x = true.
+          Proof.
+            eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; try eassumption;
+              eapply tighter_than_union.
+          Qed.
+
+          Lemma is_bounded_by_union_r t (rx ry : ZRange.type.base.option.interp t) y :
+            ZRange.type.base.option.is_bounded_by ry y = true ->
+            ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union rx ry) y = true.
+          Proof.
+            eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; try eassumption;
+              eapply tighter_than_union.
+          Qed.
         End option.
       End base.
 
@@ -484,6 +540,16 @@ Module Compilers.
                            | [ H : (forall a b, ?R0 a b = true -> forall c d, ?R1 c d = true -> forall e f, (forall g h, ?R3 g h = true -> ?R4 (e g) (f h) = true) -> forall i j, ?R5 i j = true -> ?R6 (?F _ _ _ _) (?G _ _ _ _) = true)
                                |- ?R6 (?F _ _ _ _) (?G _ _ _ _) = true ]
                              => apply H; clear H
+                           end
+                         | match goal with
+                           | [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.Thunked.bool_rect _ _ _ true) = true ]
+                             => apply ZRange.type.base.option.is_bounded_by_union_l
+                           | [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.Thunked.bool_rect _ _ _ false) = true ]
+                             => apply ZRange.type.base.option.is_bounded_by_union_r
+                           | [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.bool_rect_nodep _ _ true) = true ]
+                             => apply ZRange.type.base.option.is_bounded_by_union_l
+                           | [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.bool_rect_nodep _ _ false) = true ]
+                             => apply ZRange.type.base.option.is_bounded_by_union_r
                            end ].
 
           Local Lemma mul_by_halves_bounds x y n :
@@ -751,6 +817,7 @@ Module Compilers.
                              end
                            | intros; mul_by_halves_t ].
             all: try solve [ non_arith_t; Z.ltb_to_lt; reflexivity ].
+            all: try solve [ cbv [ZRange.ToConstant.four_corners ZRange.ToConstant.Option.four_corners ZRange.ToConstant.Option.apply_to_range ZRange.ToConstant.Option.two_corners ZRange.ToConstant.Option.union option_beq Bool.eqb] in *; non_arith_t; Z.ltb_to_lt; lia ].
             (** For command-line debugging, we display goals that should not remain *)
             all: [ > idtac "WARNING: Remaining goal:"; print_context_and_goal () .. ].
           Qed.