Add some ZUtil/Land/Fold.v lemmas (#1487)

src/Util/ZUtil.v

@@ -18,6 +18,7 @@ Require Crypto.Util.ZUtil.Hints.PullPush.
 Require Crypto.Util.ZUtil.Hints.ZArith.
 Require Crypto.Util.ZUtil.Hints.Ztestbit.
 Require Crypto.Util.ZUtil.Land.
+Require Crypto.Util.ZUtil.Land.Fold.
 Require Crypto.Util.ZUtil.LandLorBounds.
 Require Crypto.Util.ZUtil.LandLorShiftBounds.
 Require Crypto.Util.ZUtil.Lor.

src/Util/ZUtil/Land/Fold.v

@@ -0,0 +1,25 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
+Require Import Coq.Lists.List.
+Require Import Crypto.Util.ZUtil.Land.
+Require Import Crypto.Util.ZUtil.Hints.Core.
+Local Open Scope bool_scope. Local Open Scope Z_scope.
+
+Module Z.
+  Lemma fold_right_land_m1_cps v ls
+    : fold_right Z.land v ls
+      = Z.land (fold_right Z.land (-1) ls) v.
+  Proof.
+    induction ls as [|?? IH]; cbn [fold_right].
+    { now rewrite Z.land_m1'_l. }
+    { rewrite <- !Z.land_assoc, IH; reflexivity. }
+  Qed.
+
+  Lemma fold_right_land_ones_id sz ls
+    : Z.land (fold_right Z.land (Z.ones sz) ls) (Z.ones sz)
+      = Z.land (fold_right Z.land (-1) ls) (Z.ones sz).
+  Proof.
+    rewrite fold_right_land_m1_cps, <- Z.land_assoc, Z.land_diag.
+    reflexivity.
+  Qed.
+End Z.