Require Import BinInt.
Require Import Lia.
Require Import ZBinary.

From compcert Require Import Integers Coqlib.

Require Import Vericertlib.

Local Open Scope Z_scope.

Module PtrofsExtra.

  Ltac ptrofs_mod_match m :=
    match goal with
    | [ H : ?x = 0 |- context[?x] ] => rewrite H
    | [ _ : _ |- context[_ - 0] ] => rewrite Z.sub_0_r
    | [ _ : _ |- context[0 + _] ] => rewrite Z.add_0_l
    | [ _ : _ |- context[_ + 0] ] => rewrite Z.add_0_r
    | [ _ : _ |- context[0 * _] ] => rewrite Z.mul_0_l
    | [ _ : _ |- context[_ * 0] ] => rewrite Z.mul_0_r
    | [ _ : _ |- context[?m mod ?m] ] =>
      rewrite Z_mod_same_full with (a := m)
    | [ _ : _ |- context[0 mod _] ] =>
      rewrite Z.mod_0_l
    | [ _ : _ |- context[(_ mod ?m) mod ?m] ] =>
      rewrite Zmod_mod
    | [ _ : _ |- context[(_ mod Ptrofs.modulus) mod m ] ] =>
      rewrite <- Zmod_div_mod;
      try (crush; lia || assumption)

    | [ _ : _ |- context[Ptrofs.modulus mod m] ] =>
      rewrite Zdivide_mod with (a := Ptrofs.modulus);
      try (lia || assumption)

    | [ _ : _ |- context[Ptrofs.signed ?a mod Ptrofs.modulus] ] =>
      rewrite Z.mod_small with (a := Ptrofs.signed a) (b := Ptrofs.modulus)

    | [ _ : _ |- context[(?x - ?y) mod ?m] ] =>
      rewrite Zminus_mod with (a := x) (b := y) (n := m)

    | [ _ : _ |- context[((?x + ?y) mod ?m) + _] ] =>
      rewrite Zplus_mod with (a := x) (b := y) (n := m)
    | [ _ : _ |- context[(?x + ?y) mod ?m] ] =>
      rewrite Zplus_mod with (a := x) (b := y) (n := m)

    | [ _ : _ |- context[(?x * ?y) mod ?m] ] =>
      rewrite Zmult_mod with (a := x) (b := y) (n := m)
    end.

  Ltac ptrofs_mod_tac m :=
    repeat (ptrofs_mod_match m); lia.

  Lemma signed_mod_unsigned_mod :
    forall x m,
      0 < m ->
      Ptrofs.modulus mod m = 0 ->
      Ptrofs.signed x mod m = 0 ->
      Ptrofs.unsigned x mod m = 0.
forall (x : ptrofs) (m : Z),
0 < m ->
Ptrofs.modulus mod m = 0 ->
Ptrofs.signed x mod m = 0 ->
Ptrofs.unsigned x mod m = 0
  Proof.
forall (x : ptrofs) (m : Z),
0 < m ->
Ptrofs.modulus mod m = 0 ->
Ptrofs.signed x mod m = 0 ->
Ptrofs.unsigned x mod m = 0
    intros.
x:ptrofs
m:Z
H:0 < m
H0:Ptrofs.modulus mod m = 0
H1:Ptrofs.signed x mod m = 0
Ptrofs.unsigned x mod m = 0

    repeat match goal with
           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
           | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] =>
             rewrite <- Zmod_div_mod; try lia; try assumption
           | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed
           end; try crush; ptrofs_mod_tac m.
  Qed.

  Lemma of_int_mod :
    forall x m,
      Int.unsigned x mod m = 0 ->
      Ptrofs.unsigned (Ptrofs.of_int x) mod m = 0.
forall (x : int) (m : Z),
Int.unsigned x mod m = 0 ->
Ptrofs.unsigned (Ptrofs.of_int x) mod m = 0
  Proof.
forall (x : int) (m : Z),
Int.unsigned x mod m = 0 ->
Ptrofs.unsigned (Ptrofs.of_int x) mod m = 0
    intros.
x:int
m:Z
H:Int.unsigned x mod m = 0
Ptrofs.unsigned (Ptrofs.of_int x) mod m = 0
    unfold Ptrofs.of_int.
x:int
m:Z
H:Int.unsigned x mod m = 0
Ptrofs.unsigned (Ptrofs.repr (Int.unsigned x)) mod m =
0
    rewrite Ptrofs.unsigned_repr; crush;
      apply Int.unsigned_range_2.
  Qed.

  Lemma mul_mod :
    forall x y m,
      0 < m ->
      (m | Ptrofs.modulus) ->
      Ptrofs.unsigned x mod m = 0 ->
      Ptrofs.unsigned y mod m = 0 ->
      (Ptrofs.signed (Ptrofs.mul x y)) mod m = 0.
forall (x y : ptrofs) (m : Z),
0 < m ->
(m | Ptrofs.modulus) ->
Ptrofs.unsigned x mod m = 0 ->
Ptrofs.unsigned y mod m = 0 ->
Ptrofs.signed (Ptrofs.mul x y) mod m = 0
  Proof.
forall (x y : ptrofs) (m : Z),
0 < m ->
(m | Ptrofs.modulus) ->
Ptrofs.unsigned x mod m = 0 ->
Ptrofs.unsigned y mod m = 0 ->
Ptrofs.signed (Ptrofs.mul x y) mod m = 0
    intros.
x, y:ptrofs
m:Z
H:0 < m
H0:(m | Ptrofs.modulus)
H1:Ptrofs.unsigned x mod m = 0
H2:Ptrofs.unsigned y mod m = 0
Ptrofs.signed (Ptrofs.mul x y) mod m = 0 unfold Ptrofs.mul.
x, y:ptrofs
m:Z
H:0 < m
H0:(m | Ptrofs.modulus)
H1:Ptrofs.unsigned x mod m = 0
H2:Ptrofs.unsigned y mod m = 0
Ptrofs.signed
  (Ptrofs.repr (Ptrofs.unsigned x * Ptrofs.unsigned y))
mod m = 0
    rewrite Ptrofs.signed_repr_eq.
x, y:ptrofs
m:Z
H:0 < m
H0:(m | Ptrofs.modulus)
H1:Ptrofs.unsigned x mod m = 0
H2:Ptrofs.unsigned y mod m = 0
(if
  zlt
    ((Ptrofs.unsigned x * Ptrofs.unsigned y)
     mod Ptrofs.modulus) Ptrofs.half_modulus
 then
  (Ptrofs.unsigned x * Ptrofs.unsigned y)
  mod Ptrofs.modulus
 else
  (Ptrofs.unsigned x * Ptrofs.unsigned y)
  mod Ptrofs.modulus - Ptrofs.modulus) mod m = 0

    repeat match goal with
           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
           | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] =>
             rewrite <- Zmod_div_mod; try lia; try assumption
           end; try(crush; lia); ptrofs_mod_tac m.
  Qed.

  Lemma add_mod :
    forall x y m,
      0 < m ->
      (m | Ptrofs.modulus) ->
      Ptrofs.unsigned x mod m = 0 ->
      Ptrofs.unsigned y mod m = 0 ->
      (Ptrofs.unsigned (Ptrofs.add x y)) mod m = 0.
forall (x y : ptrofs) (m : Z),
0 < m ->
(m | Ptrofs.modulus) ->
Ptrofs.unsigned x mod m = 0 ->
Ptrofs.unsigned y mod m = 0 ->
Ptrofs.unsigned (Ptrofs.add x y) mod m = 0
  Proof.
forall (x y : ptrofs) (m : Z),
0 < m ->
(m | Ptrofs.modulus) ->
Ptrofs.unsigned x mod m = 0 ->
Ptrofs.unsigned y mod m = 0 ->
Ptrofs.unsigned (Ptrofs.add x y) mod m = 0
    intros.
x, y:ptrofs
m:Z
H:0 < m
H0:(m | Ptrofs.modulus)
H1:Ptrofs.unsigned x mod m = 0
H2:Ptrofs.unsigned y mod m = 0
Ptrofs.unsigned (Ptrofs.add x y) mod m = 0 unfold Ptrofs.add.
x, y:ptrofs
m:Z
H:0 < m
H0:(m | Ptrofs.modulus)
H1:Ptrofs.unsigned x mod m = 0
H2:Ptrofs.unsigned y mod m = 0
Ptrofs.unsigned
  (Ptrofs.repr (Ptrofs.unsigned x + Ptrofs.unsigned y))
mod m = 0
    rewrite Ptrofs.unsigned_repr_eq.
x, y:ptrofs
m:Z
H:0 < m
H0:(m | Ptrofs.modulus)
H1:Ptrofs.unsigned x mod m = 0
H2:Ptrofs.unsigned y mod m = 0
((Ptrofs.unsigned x + Ptrofs.unsigned y)
 mod Ptrofs.modulus) mod m = 0

    repeat match goal with
           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
           | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] =>
             rewrite <- Zmod_div_mod; try lia; try assumption
           end; try (crush; lia); ptrofs_mod_tac m.
  Qed.

  Lemma mul_divu :
    forall x y,
      0 < Ptrofs.unsigned x ->
      Ptrofs.unsigned y mod Ptrofs.unsigned x = 0 ->
      (Integers.Ptrofs.mul x (Integers.Ptrofs.divu y x)) = y.
forall x y : ptrofs,
0 < Ptrofs.unsigned x ->
Ptrofs.unsigned y mod Ptrofs.unsigned x = 0 ->
Ptrofs.mul x (Ptrofs.divu y x) = y
  Proof.
forall x y : ptrofs,
0 < Ptrofs.unsigned x ->
Ptrofs.unsigned y mod Ptrofs.unsigned x = 0 ->
Ptrofs.mul x (Ptrofs.divu y x) = y
    intros.
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
Ptrofs.mul x (Ptrofs.divu y x) = y

    assert (x <> Ptrofs.zero).
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
x <> Ptrofs.zero
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x <> Ptrofs.zero
Ptrofs.mul x (Ptrofs.divu y x) = y
    {
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
x <> Ptrofs.zero intro.
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x = Ptrofs.zero
False
      rewrite H1 in H.
x, y:ptrofs
H:0 < Ptrofs.unsigned Ptrofs.zero
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x = Ptrofs.zero
False
      replace (Ptrofs.unsigned Ptrofs.zero) with 0 in H by reflexivity.
x, y:ptrofs
H:0 < 0
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x = Ptrofs.zero
False
      lia. }
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x <> Ptrofs.zero
Ptrofs.mul x (Ptrofs.divu y x) = y

    exploit (Ptrofs.modu_divu_Euclid y x); auto; intros.
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x <> Ptrofs.zero
H2:y =
Ptrofs.add (Ptrofs.mul (Ptrofs.divu y x) x)
  (Ptrofs.modu y x)
Ptrofs.mul x (Ptrofs.divu y x) = y
    unfold Ptrofs.modu in H2.
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x <> Ptrofs.zero
H2:y =
Ptrofs.add (Ptrofs.mul (Ptrofs.divu y x) x)
  (Ptrofs.repr
     (Ptrofs.unsigned y mod Ptrofs.unsigned x))
Ptrofs.mul x (Ptrofs.divu y x) = y rewrite H0 in H2.
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x <> Ptrofs.zero
H2:y =
Ptrofs.add (Ptrofs.mul (Ptrofs.divu y x) x)
  (Ptrofs.repr 0)
Ptrofs.mul x (Ptrofs.divu y x) = y
    replace (Ptrofs.repr 0) with Ptrofs.zero in H2 by reflexivity.
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x <> Ptrofs.zero
H2:y =
Ptrofs.add (Ptrofs.mul (Ptrofs.divu y x) x)
  Ptrofs.zero
Ptrofs.mul x (Ptrofs.divu y x) = y
    rewrite Ptrofs.add_zero in H2.
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x <> Ptrofs.zero
H2:y = Ptrofs.mul (Ptrofs.divu y x) x
Ptrofs.mul x (Ptrofs.divu y x) = y
    rewrite Ptrofs.mul_commut.
x, y:ptrofs
H:0 < Ptrofs.unsigned x
H0:Ptrofs.unsigned y mod Ptrofs.unsigned x = 0
H1:x <> Ptrofs.zero
H2:y = Ptrofs.mul (Ptrofs.divu y x) x
Ptrofs.mul (Ptrofs.divu y x) x = y
    congruence.
  Qed.

  Lemma divu_unsigned :
    forall x y,
      0 < Ptrofs.unsigned y ->
      Ptrofs.unsigned x <= Ptrofs.max_unsigned ->
      Ptrofs.unsigned (Ptrofs.divu x y) = Ptrofs.unsigned x / Ptrofs.unsigned y.
forall x y : ptrofs,
0 < Ptrofs.unsigned y ->
Ptrofs.unsigned x <= Ptrofs.max_unsigned ->
Ptrofs.unsigned (Ptrofs.divu x y) =
Ptrofs.unsigned x / Ptrofs.unsigned y
  Proof.
forall x y : ptrofs,
0 < Ptrofs.unsigned y ->
Ptrofs.unsigned x <= Ptrofs.max_unsigned ->
Ptrofs.unsigned (Ptrofs.divu x y) =
Ptrofs.unsigned x / Ptrofs.unsigned y
    intros.
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
Ptrofs.unsigned (Ptrofs.divu x y) =
Ptrofs.unsigned x / Ptrofs.unsigned y
    unfold Ptrofs.divu.
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
Ptrofs.unsigned
  (Ptrofs.repr (Ptrofs.unsigned x / Ptrofs.unsigned y)) =
Ptrofs.unsigned x / Ptrofs.unsigned y
    rewrite Ptrofs.unsigned_repr; auto.
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
0 <= Ptrofs.unsigned x / Ptrofs.unsigned y <=
Ptrofs.max_unsigned
    split.
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
0 <= Ptrofs.unsigned x / Ptrofs.unsigned y
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
Ptrofs.unsigned x / Ptrofs.unsigned y <=
Ptrofs.max_unsigned
    apply Z.div_pos; auto.
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
0 <= Ptrofs.unsigned x
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
Ptrofs.unsigned x / Ptrofs.unsigned y <=
Ptrofs.max_unsigned
    apply Ptrofs.unsigned_range.
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
Ptrofs.unsigned x / Ptrofs.unsigned y <=
Ptrofs.max_unsigned
    apply Z.div_le_upper_bound; auto.
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
Ptrofs.unsigned x <=
Ptrofs.unsigned y * Ptrofs.max_unsigned
    eapply Z.le_trans.
    exact H0.
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
Ptrofs.max_unsigned <=
Ptrofs.unsigned y * Ptrofs.max_unsigned
    rewrite Z.mul_comm.
x, y:ptrofs
H:0 < Ptrofs.unsigned y
H0:Ptrofs.unsigned x <= Ptrofs.max_unsigned
Ptrofs.max_unsigned <=
Ptrofs.max_unsigned * Ptrofs.unsigned y
    apply Z.le_mul_diag_r; crush.
  Qed.

  Lemma mul_unsigned :
    forall x y,
      Ptrofs.mul x y =
      Ptrofs.repr (Ptrofs.unsigned x * Ptrofs.unsigned y).
forall x y : ptrofs,
Ptrofs.mul x y =
Ptrofs.repr (Ptrofs.unsigned x * Ptrofs.unsigned y)
  Proof.
forall x y : ptrofs,
Ptrofs.mul x y =
Ptrofs.repr (Ptrofs.unsigned x * Ptrofs.unsigned y)
    intros; unfold Ptrofs.mul.
x, y:ptrofs
Ptrofs.repr (Ptrofs.unsigned x * Ptrofs.unsigned y) =
Ptrofs.repr (Ptrofs.unsigned x * Ptrofs.unsigned y)
    apply Ptrofs.eqm_samerepr.
x, y:ptrofs
Ptrofs.eqm (Ptrofs.unsigned x * Ptrofs.unsigned y)
  (Ptrofs.unsigned x * Ptrofs.unsigned y)
    apply Ptrofs.eqm_mult; exists 0; lia.
  Qed.

  Lemma pos_signed_unsigned :
    forall x,
      0 <= Ptrofs.signed x ->
      Ptrofs.signed x = Ptrofs.unsigned x.
forall x : ptrofs,
0 <= Ptrofs.signed x ->
Ptrofs.signed x = Ptrofs.unsigned x
  Proof.
forall x : ptrofs,
0 <= Ptrofs.signed x ->
Ptrofs.signed x = Ptrofs.unsigned x
    intros.
x:ptrofs
H:0 <= Ptrofs.signed x
Ptrofs.signed x = Ptrofs.unsigned x
    rewrite Ptrofs.unsigned_signed.
x:ptrofs
H:0 <= Ptrofs.signed x
Ptrofs.signed x =
(if Ptrofs.lt x Ptrofs.zero
 then Ptrofs.signed x + Ptrofs.modulus
 else Ptrofs.signed x)
    destruct (Ptrofs.lt x Ptrofs.zero) eqn:EQ.
x:ptrofs
H:0 <= Ptrofs.signed x
EQ:Ptrofs.lt x Ptrofs.zero = true
Ptrofs.signed x = Ptrofs.signed x + Ptrofs.modulus
x:ptrofs
H:0 <= Ptrofs.signed x
EQ:Ptrofs.lt x Ptrofs.zero = false
Ptrofs.signed x = Ptrofs.signed x
    unfold Ptrofs.lt in EQ.
x:ptrofs
H:0 <= Ptrofs.signed x
EQ:(if
  zlt (Ptrofs.signed x)
    (Ptrofs.signed Ptrofs.zero)
 then true
 else false) = true
Ptrofs.signed x = Ptrofs.signed x + Ptrofs.modulus
x:ptrofs
H:0 <= Ptrofs.signed x
EQ:Ptrofs.lt x Ptrofs.zero = false
Ptrofs.signed x = Ptrofs.signed x
    destruct (zlt (Ptrofs.signed x) (Ptrofs.signed Ptrofs.zero)); try discriminate.
x:ptrofs
H:0 <= Ptrofs.signed x
l:Ptrofs.signed x < Ptrofs.signed Ptrofs.zero
EQ:true = true
Ptrofs.signed x = Ptrofs.signed x + Ptrofs.modulus
x:ptrofs
H:0 <= Ptrofs.signed x
EQ:Ptrofs.lt x Ptrofs.zero = false
Ptrofs.signed x = Ptrofs.signed x
    replace (Ptrofs.signed (Ptrofs.zero)) with 0 in l by reflexivity.
x:ptrofs
H:0 <= Ptrofs.signed x
l:Ptrofs.signed x < 0
EQ:true = true
Ptrofs.signed x = Ptrofs.signed x + Ptrofs.modulus
x:ptrofs
H:0 <= Ptrofs.signed x
EQ:Ptrofs.lt x Ptrofs.zero = false
Ptrofs.signed x = Ptrofs.signed x lia.
x:ptrofs
H:0 <= Ptrofs.signed x
EQ:Ptrofs.lt x Ptrofs.zero = false
Ptrofs.signed x = Ptrofs.signed x
    reflexivity.
  Qed.
End PtrofsExtra.

Ltac ptrofs :=
  repeat match goal with
         | [ |- context[Ptrofs.add (Ptrofs.zero) _] ] => setoid_rewrite Ptrofs.add_zero_l
         | [ H : context[Ptrofs.add (Ptrofs.zero) _] |- _ ] => setoid_rewrite Ptrofs.add_zero_l in H

         | [ |- context[Ptrofs.repr 0] ] => replace (Ptrofs.repr 0) with Ptrofs.zero by reflexivity
         | [ H : context[Ptrofs.repr 0] |- _ ] =>
           replace (Ptrofs.repr 0) with Ptrofs.zero in H by reflexivity

         | [ H: context[Ptrofs.unsigned (Ptrofs.repr (Ptrofs.unsigned _))] |- _ ] =>
           setoid_rewrite Ptrofs.unsigned_repr in H; [>| apply Ptrofs.unsigned_range_2]
         | [ |- context[Ptrofs.unsigned (Ptrofs.repr (Ptrofs.unsigned _))] ] =>
           rewrite Ptrofs.unsigned_repr; [>| apply Ptrofs.unsigned_range_2]

         | [ |- context[0 <= Ptrofs.unsigned _] ] => apply Ptrofs.unsigned_range_2
         end.

Module IntExtra.
  Import Int.
  Ltac int_mod_match m :=
    match goal with
    | [ H : ?x = 0 |- context[?x] ] => rewrite H
    | [ _ : _ |- context[_ - 0] ] => rewrite Z.sub_0_r
    | [ _ : _ |- context[0 + _] ] => rewrite Z.add_0_l
    | [ _ : _ |- context[_ + 0] ] => rewrite Z.add_0_r
    | [ _ : _ |- context[0 * _] ] => rewrite Z.mul_0_l
    | [ _ : _ |- context[_ * 0] ] => rewrite Z.mul_0_r
    | [ _ : _ |- context[?m mod ?m] ] =>
      rewrite Z_mod_same_full with (a := m)
    | [ _ : _ |- context[0 mod _] ] =>
      rewrite Z.mod_0_l
    | [ _ : _ |- context[(_ mod ?m) mod ?m] ] =>
      rewrite Zmod_mod
    | [ _ : _ |- context[(_ mod Int.modulus) mod m ] ] =>
      rewrite <- Zmod_div_mod;
      try (crush; lia || assumption)

    | [ _ : _ |- context[Int.modulus mod m] ] =>
      rewrite Zdivide_mod with (a := Int.modulus);
      try (lia || assumption)

    | [ _ : _ |- context[Int.signed ?a mod Int.modulus] ] =>
      rewrite Z.mod_small with (a := Int.signed a) (b := Int.modulus)

    | [ _ : _ |- context[(?x - ?y) mod ?m] ] =>
      rewrite Zminus_mod with (a := x) (b := y) (n := m)

    | [ _ : _ |- context[((?x + ?y) mod ?m) + _] ] =>
      rewrite Zplus_mod with (a := x) (b := y) (n := m)
    | [ _ : _ |- context[(?x + ?y) mod ?m] ] =>
      rewrite Zplus_mod with (a := x) (b := y) (n := m)

    | [ _ : _ |- context[(?x * ?y) mod ?m] ] =>
      rewrite Zmult_mod with (a := x) (b := y) (n := m)
    end.

  Ltac int_mod_tac m :=
    repeat (int_mod_match m); lia.

  Lemma mul_mod1 :
    forall x y m,
      0 < m ->
      (m | Int.modulus) ->
      Int.unsigned x mod m = 0 ->
      (Int.unsigned (Int.mul x y)) mod m = 0.
forall (x y : Integers.int) (m : Z),
0 < m ->
(m | modulus) ->
unsigned x mod m = 0 -> unsigned (mul x y) mod m = 0
  Proof.
forall (x y : Integers.int) (m : Z),
0 < m ->
(m | modulus) ->
unsigned x mod m = 0 -> unsigned (mul x y) mod m = 0
    intros.
x, y:Integers.int
m:Z
H:0 < m
H0:(m | modulus)
H1:unsigned x mod m = 0
unsigned (mul x y) mod m = 0 unfold Int.mul.
x, y:Integers.int
m:Z
H:0 < m
H0:(m | modulus)
H1:unsigned x mod m = 0
unsigned (repr (unsigned x * unsigned y)) mod m = 0
    rewrite Int.unsigned_repr_eq.
x, y:Integers.int
m:Z
H:0 < m
H0:(m | modulus)
H1:unsigned x mod m = 0
((unsigned x * unsigned y) mod modulus) mod m = 0

    repeat match goal with
           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
           | [ _ : _ |- context[_ mod Int.modulus mod m] ] =>
             rewrite <- Zmod_div_mod; try lia; try assumption
           end; try (crush; lia); int_mod_tac m.
  Qed.

  Lemma mul_mod2 :
    forall x y m,
      0 < m ->
      (m | Int.modulus) ->
      Int.unsigned y mod m = 0 ->
      (Int.unsigned (Int.mul x y)) mod m = 0.
forall (x y : Integers.int) (m : Z),
0 < m ->
(m | modulus) ->
unsigned y mod m = 0 -> unsigned (mul x y) mod m = 0
  Proof.
forall (x y : Integers.int) (m : Z),
0 < m ->
(m | modulus) ->
unsigned y mod m = 0 -> unsigned (mul x y) mod m = 0
    intros.
x, y:Integers.int
m:Z
H:0 < m
H0:(m | modulus)
H1:unsigned y mod m = 0
unsigned (mul x y) mod m = 0 unfold Int.mul.
x, y:Integers.int
m:Z
H:0 < m
H0:(m | modulus)
H1:unsigned y mod m = 0
unsigned (repr (unsigned x * unsigned y)) mod m = 0
    rewrite Int.unsigned_repr_eq.
x, y:Integers.int
m:Z
H:0 < m
H0:(m | modulus)
H1:unsigned y mod m = 0
((unsigned x * unsigned y) mod modulus) mod m = 0

    repeat match goal with
           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
           | [ _ : _ |- context[_ mod Int.modulus mod m] ] =>
             rewrite <- Zmod_div_mod; try lia; try assumption
           end; try (crush; lia); int_mod_tac m.
  Qed.

  Lemma add_mod :
    forall x y m,
      0 < m ->
      (m | Int.modulus) ->
      Int.unsigned x mod m = 0 ->
      Int.unsigned y mod m = 0 ->
      (Int.unsigned (Int.add x y)) mod m = 0.
forall (x y : Integers.int) (m : Z),
0 < m ->
(m | modulus) ->
unsigned x mod m = 0 ->
unsigned y mod m = 0 -> unsigned (add x y) mod m = 0
  Proof.
forall (x y : Integers.int) (m : Z),
0 < m ->
(m | modulus) ->
unsigned x mod m = 0 ->
unsigned y mod m = 0 -> unsigned (add x y) mod m = 0
    intros.
x, y:Integers.int
m:Z
H:0 < m
H0:(m | modulus)
H1:unsigned x mod m = 0
H2:unsigned y mod m = 0
unsigned (add x y) mod m = 0 unfold Int.add.
x, y:Integers.int
m:Z
H:0 < m
H0:(m | modulus)
H1:unsigned x mod m = 0
H2:unsigned y mod m = 0
unsigned (repr (unsigned x + unsigned y)) mod m = 0
    rewrite Int.unsigned_repr_eq.
x, y:Integers.int
m:Z
H:0 < m
H0:(m | modulus)
H1:unsigned x mod m = 0
H2:unsigned y mod m = 0
((unsigned x + unsigned y) mod modulus) mod m = 0

    repeat match goal with
           | [ _ : _ |- context[if ?x then _ else _] ] => destruct x
           | [ _ : _ |- context[_ mod Int.modulus mod m] ] =>
             rewrite <- Zmod_div_mod; try lia; try assumption
           end; try (crush; lia); int_mod_tac m.
  Qed.

  Definition ofbytes (a b c d : byte) : int :=
    or (shl (repr (Byte.unsigned a)) (repr (3 * Byte.zwordsize)))
       (or (shl (repr (Byte.unsigned b)) (repr (2 * Byte.zwordsize)))
           (or (shl (repr (Byte.unsigned c)) (repr Byte.zwordsize))
               (repr (Byte.unsigned d)))).

  Definition byte1 (n: int) : byte := Byte.repr (unsigned n).

  Definition byte2 (n: int) : byte := Byte.repr (unsigned (shru n (repr Byte.zwordsize))).

  Definition byte3 (n: int) : byte := Byte.repr (unsigned (shru n (repr (2 * Byte.zwordsize)))).

  Definition byte4 (n: int) : byte := Byte.repr (unsigned (shru n (repr (3 * Byte.zwordsize)))).

  Lemma bits_byte1:
    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte1 n) i = testbit n i.
forall (n : Integers.int) (i : Z),
0 <= i < Byte.zwordsize ->
Byte.testbit (byte1 n) i = testbit n i
  Proof.
forall (n : Integers.int) (i : Z),
0 <= i < Byte.zwordsize ->
Byte.testbit (byte1 n) i = testbit n i
    intros.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Byte.testbit (byte1 n) i = testbit n i unfold byte1.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Byte.testbit (Byte.repr (unsigned n)) i = testbit n i rewrite Byte.testbit_repr; auto.
  Qed.

  Lemma bits_byte2:
    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte2 n) i = testbit n (i + Byte.zwordsize).
forall (n : Integers.int) (i : Z),
0 <= i < Byte.zwordsize ->
Byte.testbit (byte2 n) i =
testbit n (i + Byte.zwordsize)
  Proof.
forall (n : Integers.int) (i : Z),
0 <= i < Byte.zwordsize ->
Byte.testbit (byte2 n) i =
testbit n (i + Byte.zwordsize)
    intros.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Byte.testbit (byte2 n) i =
testbit n (i + Byte.zwordsize) unfold byte2.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Byte.testbit
  (Byte.repr (unsigned (shru n (repr Byte.zwordsize))))
  i = testbit n (i + Byte.zwordsize) rewrite Byte.testbit_repr; auto.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Z.testbit (unsigned (shru n (repr Byte.zwordsize))) i =
testbit n (i + Byte.zwordsize)
    assert (zwordsize = 4 * Byte.zwordsize) by reflexivity.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
Z.testbit (unsigned (shru n (repr Byte.zwordsize))) i =
testbit n (i + Byte.zwordsize)
    fold (testbit (shru n (repr Byte.zwordsize)) i).
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
testbit (shru n (repr Byte.zwordsize)) i =
testbit n (i + Byte.zwordsize) rewrite bits_shru.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
(if zlt (i + unsigned (repr Byte.zwordsize)) zwordsize
 then testbit n (i + unsigned (repr Byte.zwordsize))
 else false) = testbit n (i + Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
    change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
(if zlt (i + Byte.zwordsize) zwordsize
 then testbit n (i + Byte.zwordsize)
 else false) = testbit n (i + Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
    apply zlt_true.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
i + Byte.zwordsize < zwordsize
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize omega.
omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize omega.
omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
  Qed.

  Lemma bits_byte3:
    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte3 n) i = testbit n (i + (2 * Byte.zwordsize)).
forall (n : Integers.int) (i : Z),
0 <= i < Byte.zwordsize ->
Byte.testbit (byte3 n) i =
testbit n (i + 2 * Byte.zwordsize)
  Proof.
forall (n : Integers.int) (i : Z),
0 <= i < Byte.zwordsize ->
Byte.testbit (byte3 n) i =
testbit n (i + 2 * Byte.zwordsize)
    intros.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Byte.testbit (byte3 n) i =
testbit n (i + 2 * Byte.zwordsize) unfold byte3.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Byte.testbit
  (Byte.repr
     (unsigned (shru n (repr (2 * Byte.zwordsize)))))
  i = testbit n (i + 2 * Byte.zwordsize) rewrite Byte.testbit_repr; auto.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Z.testbit
  (unsigned (shru n (repr (2 * Byte.zwordsize)))) i =
testbit n (i + 2 * Byte.zwordsize)
    assert (zwordsize = 4 * Byte.zwordsize) by reflexivity.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
Z.testbit
  (unsigned (shru n (repr (2 * Byte.zwordsize)))) i =
testbit n (i + 2 * Byte.zwordsize)
    fold (testbit (shru n (repr (2 * Byte.zwordsize))) i).
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
testbit (shru n (repr (2 * Byte.zwordsize))) i =
testbit n (i + 2 * Byte.zwordsize) rewrite bits_shru.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
(if
  zlt (i + unsigned (repr (2 * Byte.zwordsize)))
    zwordsize
 then
  testbit n (i + unsigned (repr (2 * Byte.zwordsize)))
 else false) = testbit n (i + 2 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
    change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize).
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
(if zlt (i + 2 * Byte.zwordsize) zwordsize
 then testbit n (i + 2 * Byte.zwordsize)
 else false) = testbit n (i + 2 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
    apply zlt_true.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
i + 2 * Byte.zwordsize < zwordsize
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize omega.
omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize omega.
omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
  Qed.

  Lemma bits_byte4:
    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte4 n) i = testbit n (i + (3 * Byte.zwordsize)).
forall (n : Integers.int) (i : Z),
0 <= i < Byte.zwordsize ->
Byte.testbit (byte4 n) i =
testbit n (i + 3 * Byte.zwordsize)
  Proof.
forall (n : Integers.int) (i : Z),
0 <= i < Byte.zwordsize ->
Byte.testbit (byte4 n) i =
testbit n (i + 3 * Byte.zwordsize)
    intros.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Byte.testbit (byte4 n) i =
testbit n (i + 3 * Byte.zwordsize) unfold byte4.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Byte.testbit
  (Byte.repr
     (unsigned (shru n (repr (3 * Byte.zwordsize)))))
  i = testbit n (i + 3 * Byte.zwordsize) rewrite Byte.testbit_repr; auto.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
Z.testbit
  (unsigned (shru n (repr (3 * Byte.zwordsize)))) i =
testbit n (i + 3 * Byte.zwordsize)
    assert (zwordsize = 4 * Byte.zwordsize) by reflexivity.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
Z.testbit
  (unsigned (shru n (repr (3 * Byte.zwordsize)))) i =
testbit n (i + 3 * Byte.zwordsize)
    fold (testbit (shru n (repr (3 * Byte.zwordsize))) i).
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
testbit (shru n (repr (3 * Byte.zwordsize))) i =
testbit n (i + 3 * Byte.zwordsize) rewrite bits_shru.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
(if
  zlt (i + unsigned (repr (3 * Byte.zwordsize)))
    zwordsize
 then
  testbit n (i + unsigned (repr (3 * Byte.zwordsize)))
 else false) = testbit n (i + 3 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
    change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize).
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
(if zlt (i + 3 * Byte.zwordsize) zwordsize
 then testbit n (i + 3 * Byte.zwordsize)
 else false) = testbit n (i + 3 * Byte.zwordsize)
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize
    apply zlt_true.
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
i + 3 * Byte.zwordsize < zwordsize
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize omega.
omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
n:Integers.int
i:Z
H:0 <= i < Byte.zwordsize
H0:zwordsize = 4 * Byte.zwordsize
0 <= i < zwordsize omega.
omega is deprecated since 8.12; use “lia” instead.
[omega-is-deprecated,deprecated]
  Qed.

  Lemma bits_ofwords:
    forall b4 b3 b2 b1 i, 0 <= i < zwordsize ->
                          testbit (ofbytes b4 b3 b2 b1) i =
                          if zlt i Byte.zwordsize
                          then Byte.testbit b1 i
                          else (if zlt i (2 * Byte.zwordsize)
                                then Byte.testbit b2 (i - Byte.zwordsize)
                                else (if zlt i (3 * Byte.zwordsize)
                                      then Byte.testbit b2 (i - 2 * Byte.zwordsize)
                                      else Byte.testbit b2 (i - 3 * Byte.zwordsize))).
forall (b4 b3 b2 b1 : byte) (i : Z),
0 <= i < zwordsize ->
testbit (ofbytes b4 b3 b2 b1) i =
(if zlt i Byte.zwordsize
 then Byte.testbit b1 i
 else
  if zlt i (2 * Byte.zwordsize)
  then Byte.testbit b2 (i - Byte.zwordsize)
  else
   if zlt i (3 * Byte.zwordsize)
   then Byte.testbit b2 (i - 2 * Byte.zwordsize)
   else Byte.testbit b2 (i - 3 * Byte.zwordsize))
  Proof.
forall (b4 b3 b2 b1 : byte) (i : Z),
0 <= i < zwordsize ->
testbit (ofbytes b4 b3 b2 b1) i =
(if zlt i Byte.zwordsize
 then Byte.testbit b1 i
 else
  if zlt i (2 * Byte.zwordsize)
  then Byte.testbit b2 (i - Byte.zwordsize)
  else
   if zlt i (3 * Byte.zwordsize)
   then Byte.testbit b2 (i - 2 * Byte.zwordsize)
   else Byte.testbit b2 (i - 3 * Byte.zwordsize))
    intros.
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
testbit (ofbytes b4 b3 b2 b1) i =
(if zlt i Byte.zwordsize
 then Byte.testbit b1 i
 else
  if zlt i (2 * Byte.zwordsize)
  then Byte.testbit b2 (i - Byte.zwordsize)
  else
   if zlt i (3 * Byte.zwordsize)
   then Byte.testbit b2 (i - 2 * Byte.zwordsize)
   else Byte.testbit b2 (i - 3 * Byte.zwordsize)) unfold ofbytes.
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
testbit
  (or
     (shl (repr (Byte.unsigned b4))
        (repr (3 * Byte.zwordsize)))
     (or
        (shl (repr (Byte.unsigned b3))
           (repr (2 * Byte.zwordsize)))
        (or
           (shl (repr (Byte.unsigned b2))
              (repr Byte.zwordsize))
           (repr (Byte.unsigned b1))))) i =
(if zlt i Byte.zwordsize
 then Byte.testbit b1 i
 else
  if zlt i (2 * Byte.zwordsize)
  then Byte.testbit b2 (i - Byte.zwordsize)
  else
   if zlt i (3 * Byte.zwordsize)
   then Byte.testbit b2 (i - 2 * Byte.zwordsize)
   else Byte.testbit b2 (i - 3 * Byte.zwordsize)) repeat (rewrite bits_or; auto).
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
testbit
  (shl (repr (Byte.unsigned b4))
     (repr (3 * Byte.zwordsize))) i
|| (testbit
      (shl (repr (Byte.unsigned b3))
         (repr (2 * Byte.zwordsize))) i
    || (testbit
          (shl (repr (Byte.unsigned b2))
             (repr Byte.zwordsize)) i
        || testbit (repr (Byte.unsigned b1)) i)) =
(if zlt i Byte.zwordsize
 then Byte.testbit b1 i
 else
  if zlt i (2 * Byte.zwordsize)
  then Byte.testbit b2 (i - Byte.zwordsize)
  else
   if zlt i (3 * Byte.zwordsize)
   then Byte.testbit b2 (i - 2 * Byte.zwordsize)
   else Byte.testbit b2 (i - 3 * Byte.zwordsize)) repeat (rewrite bits_shl; auto).
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
(if zlt i (unsigned (repr (3 * Byte.zwordsize)))
 then false
 else
  testbit (repr (Byte.unsigned b4))
    (i - unsigned (repr (3 * Byte.zwordsize))))
|| ((if zlt i (unsigned (repr (2 * Byte.zwordsize)))
     then false
     else
      testbit (repr (Byte.unsigned b3))
        (i - unsigned (repr (2 * Byte.zwordsize))))
    || ((if zlt i (unsigned (repr Byte.zwordsize))
         then false
         else
          testbit (repr (Byte.unsigned b2))
            (i - unsigned (repr Byte.zwordsize)))
        || testbit (repr (Byte.unsigned b1)) i)) =
(if zlt i Byte.zwordsize
 then Byte.testbit b1 i
 else
  if zlt i (2 * Byte.zwordsize)
  then Byte.testbit b2 (i - Byte.zwordsize)
  else
   if zlt i (3 * Byte.zwordsize)
   then Byte.testbit b2 (i - 2 * Byte.zwordsize)
   else Byte.testbit b2 (i - 3 * Byte.zwordsize))
    change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize.
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
(if zlt i (unsigned (repr (3 * Byte.zwordsize)))
 then false
 else
  testbit (repr (Byte.unsigned b4))
    (i - unsigned (repr (3 * Byte.zwordsize))))
|| ((if zlt i (unsigned (repr (2 * Byte.zwordsize)))
     then false
     else
      testbit (repr (Byte.unsigned b3))
        (i - unsigned (repr (2 * Byte.zwordsize))))
    || ((if zlt i Byte.zwordsize
         then false
         else
          testbit (repr (Byte.unsigned b2))
            (i - Byte.zwordsize))
        || testbit (repr (Byte.unsigned b1)) i)) =
(if zlt i Byte.zwordsize
 then Byte.testbit b1 i
 else
  if zlt i (2 * Byte.zwordsize)
  then Byte.testbit b2 (i - Byte.zwordsize)
  else
   if zlt i (3 * Byte.zwordsize)
   then Byte.testbit b2 (i - 2 * Byte.zwordsize)
   else Byte.testbit b2 (i - 3 * Byte.zwordsize))
    change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize).
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
(if zlt i (unsigned (repr (3 * Byte.zwordsize)))
 then false
 else
  testbit (repr (Byte.unsigned b4))
    (i - unsigned (repr (3 * Byte.zwordsize))))
|| ((if zlt i (2 * Byte.zwordsize)
     then false
     else
      testbit (repr (Byte.unsigned b3))
        (i - 2 * Byte.zwordsize))
    || ((if zlt i Byte.zwordsize
         then false
         else
          testbit (repr (Byte.unsigned b2))
            (i - Byte.zwordsize))
        || testbit (repr (Byte.unsigned b1)) i)) =
(if zlt i Byte.zwordsize
 then Byte.testbit b1 i
 else
  if zlt i (2 * Byte.zwordsize)
  then Byte.testbit b2 (i - Byte.zwordsize)
  else
   if zlt i (3 * Byte.zwordsize)
   then Byte.testbit b2 (i - 2 * Byte.zwordsize)
   else Byte.testbit b2 (i - 3 * Byte.zwordsize))
    change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize).
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
(if zlt i (3 * Byte.zwordsize)
 then false
 else
  testbit (repr (Byte.unsigned b4))
    (i - 3 * Byte.zwordsize))
|| ((if zlt i (2 * Byte.zwordsize)
     then false
     else
      testbit (repr (Byte.unsigned b3))
        (i - 2 * Byte.zwordsize))
    || ((if zlt i Byte.zwordsize
         then false
         else
          testbit (repr (Byte.unsigned b2))
            (i - Byte.zwordsize))
        || testbit (repr (Byte.unsigned b1)) i)) =
(if zlt i Byte.zwordsize
 then Byte.testbit b1 i
 else
  if zlt i (2 * Byte.zwordsize)
  then Byte.testbit b2 (i - Byte.zwordsize)
  else
   if zlt i (3 * Byte.zwordsize)
   then Byte.testbit b2 (i - 2 * Byte.zwordsize)
   else Byte.testbit b2 (i - 3 * Byte.zwordsize))
    assert (zwordsize = 4 * Byte.zwordsize) by reflexivity.
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
H0:zwordsize = 4 * Byte.zwordsize
(if zlt i (3 * Byte.zwordsize)
 then false
 else
  testbit (repr (Byte.unsigned b4))
    (i - 3 * Byte.zwordsize))
|| ((if zlt i (2 * Byte.zwordsize)
     then false
     else
      testbit (repr (Byte.unsigned b3))
        (i - 2 * Byte.zwordsize))
    || ((if zlt i Byte.zwordsize
         then false
         else
          testbit (repr (Byte.unsigned b2))
            (i - Byte.zwordsize))
        || testbit (repr (Byte.unsigned b1)) i)) =
(if zlt i Byte.zwordsize
 then Byte.testbit b1 i
 else
  if zlt i (2 * Byte.zwordsize)
  then Byte.testbit b2 (i - Byte.zwordsize)
  else
   if zlt i (3 * Byte.zwordsize)
   then Byte.testbit b2 (i - 2 * Byte.zwordsize)
   else Byte.testbit b2 (i - 3 * Byte.zwordsize))
    destruct (zlt i Byte.zwordsize).
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
H0:zwordsize = 4 * Byte.zwordsize
l:i < Byte.zwordsize
(if zlt i (3 * Byte.zwordsize)
 then false
 else
  testbit (repr (Byte.unsigned b4))
    (i - 3 * Byte.zwordsize))
|| ((if zlt i (2 * Byte.zwordsize)
     then false
     else
      testbit (repr (Byte.unsigned b3))
        (i - 2 * Byte.zwordsize))
    || (false || testbit (repr (Byte.unsigned b1)) i)) =
Byte.testbit b1 i
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
H0:zwordsize = 4 * Byte.zwordsize
g:i >= Byte.zwordsize
(if zlt i (3 * Byte.zwordsize)
 then false
 else
  testbit (repr (Byte.unsigned b4))
    (i - 3 * Byte.zwordsize))
|| ((if zlt i (2 * Byte.zwordsize)
     then false
     else
      testbit (repr (Byte.unsigned b3))
        (i - 2 * Byte.zwordsize))
    || (testbit (repr (Byte.unsigned b2))
          (i - Byte.zwordsize)
        || testbit (repr (Byte.unsigned b1)) i)) =
(if zlt i (2 * Byte.zwordsize)
 then Byte.testbit b2 (i - Byte.zwordsize)
 else
  if zlt i (3 * Byte.zwordsize)
  then Byte.testbit b2 (i - 2 * Byte.zwordsize)
  else Byte.testbit b2 (i - 3 * Byte.zwordsize))
    rewrite testbit_repr; auto.
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
H0:zwordsize = 4 * Byte.zwordsize
l:i < Byte.zwordsize
(if zlt i (3 * Byte.zwordsize)
 then false
 else
  Z.testbit (Byte.unsigned b4)
    (i - 3 * Byte.zwordsize))
|| ((if zlt i (2 * Byte.zwordsize)
     then false
     else
      testbit (repr (Byte.unsigned b3))
        (i - 2 * Byte.zwordsize))
    || (false || testbit (repr (Byte.unsigned b1)) i)) =
Byte.testbit b1 i
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
H0:zwordsize = 4 * Byte.zwordsize
l:i < Byte.zwordsize
0 <= i - 3 * Byte.zwordsize < zwordsize
b4, b3, b2, b1:byte
i:Z
H:0 <= i < zwordsize
H0:zwordsize = 4 * Byte.zwordsize
g:i >= Byte.zwordsize
(if zlt i (3 * Byte.zwordsize)
 then false
 else
  testbit (repr (Byte.unsigned b4))
    (i - 3 * Byte.zwordsize))
|| ((if zlt i (2 * Byte.zwordsize)
     then false
     else
      testbit (repr (Byte.unsigned b3))
        (i - 2 * Byte.zwordsize))
    || (testbit (repr (Byte.unsigned b2))
          (i - Byte.zwordsize)
        || testbit (repr (Byte.unsigned b1)) i)) =
(if zlt i (2 * Byte.zwordsize)
 then Byte.testbit b2 (i - Byte.zwordsize)
 else
  if zlt i (3 * Byte.zwordsize)
  then Byte.testbit b2 (i - 2 * Byte.zwordsize)
  else Byte.testbit b2 (i - 3 * Byte.zwordsize))
    Abort.

  Lemma div_divs_equiv :
    forall x y,
      signed x >= 0 ->
      signed y >= 0 ->
      divs x y = divu x y.
forall x y : Integers.int,
signed x >= 0 -> signed y >= 0 -> divs x y = divu x y
  Proof.
forall x y : Integers.int,
signed x >= 0 -> signed y >= 0 -> divs x y = divu x y
    unfold divs, divu.
forall x y : Integers.int,
signed x >= 0 ->
signed y >= 0 ->
repr (signed x ÷ signed y) =
repr (unsigned x / unsigned y)
    intros.
x, y:Integers.int
H:signed x >= 0
H0:signed y >= 0
repr (signed x ÷ signed y) =
repr (unsigned x / unsigned y)
    rewrite !signed_eq_unsigned;
    try rewrite Zquot.Zquot_Zdiv_pos; try reflexivity;
    lazymatch goal with
    | |- unsigned _ <= max_signed =>
      solve [rewrite <- signed_positive; assumption]
    | |- 0 <= unsigned _ => solve [apply unsigned_range_2]
    end.
  Qed.

  Lemma neg_signed' :
    forall x : int,
      unsigned x <> 2147483648 ->
      signed (neg x) = - signed x.
forall x : Integers.int,
unsigned x <> 2147483648 ->
signed (neg x) = - signed x
  Proof.
forall x : Integers.int,
unsigned x <> 2147483648 ->
signed (neg x) = - signed x
    intros x Hhalf.
x:Integers.int
Hhalf:unsigned x <> 2147483648
signed (neg x) = - signed x
    Transparent repr.
x:Integers.int
Hhalf:unsigned x <> 2147483648
signed (neg x) = - signed x
    unfold signed.
x:Integers.int
Hhalf:unsigned x <> 2147483648
(if zlt (unsigned (neg x)) half_modulus
 then unsigned (neg x)
 else unsigned (neg x) - modulus) =
-
(if zlt (unsigned x) half_modulus
 then unsigned x
 else unsigned x - modulus)
    simpl.
x:Integers.int
Hhalf:unsigned x <> 2147483648
(if zlt (Z_mod_modulus (- unsigned x)) half_modulus
 then Z_mod_modulus (- unsigned x)
 else Z_mod_modulus (- unsigned x) - modulus) =
-
(if zlt (unsigned x) half_modulus
 then unsigned x
 else unsigned x - modulus)
    rewrite Z_mod_modulus_eq.
x:Integers.int
Hhalf:unsigned x <> 2147483648
(if zlt (- unsigned x mod modulus) half_modulus
 then - unsigned x mod modulus
 else - unsigned x mod modulus - modulus) =
-
(if zlt (unsigned x) half_modulus
 then unsigned x
 else unsigned x - modulus)
    replace modulus with 4294967296; auto.
x:Integers.int
Hhalf:unsigned x <> 2147483648
(if zlt (- unsigned x mod 4294967296) half_modulus
 then - unsigned x mod 4294967296
 else - unsigned x mod 4294967296 - 4294967296) =
-
(if zlt (unsigned x) half_modulus
 then unsigned x
 else unsigned x - 4294967296)
    replace half_modulus with 2147483648; auto.
x:Integers.int
Hhalf:unsigned x <> 2147483648
(if zlt (- unsigned x mod 4294967296) 2147483648
 then - unsigned x mod 4294967296
 else - unsigned x mod 4294967296 - 4294967296) =
-
(if zlt (unsigned x) 2147483648
 then unsigned x
 else unsigned x - 4294967296)
    repeat match goal with | |- context[if ?x then _ else _] => destruct x end.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
- unsigned x mod 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
- unsigned x mod 4294967296 - 4294967296 =
- unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296)
    -
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
- unsigned x mod 4294967296 = - unsigned x destruct (Z.eq_dec (unsigned x) 0).
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
e:unsigned x = 0
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 = - unsigned x
      +
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
e:unsigned x = 0
- unsigned x mod 4294967296 = - unsigned x rewrite e.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
e:unsigned x = 0
- 0 mod 4294967296 = - 0 auto.
      +
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 = - unsigned x pose proof (Z.mod_opp_l_nz (unsigned x) 4294967296).
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
- unsigned x mod 4294967296 = - unsigned x
        assert (4294967296 <> 0) by lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
- unsigned x mod 4294967296 = - unsigned x
        apply H in H0.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0
        rewrite H0 in l.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x mod 4294967296 <
2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0
        pose proof (Z.mod_small (unsigned x) 4294967296).
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x mod 4294967296 <
2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H1:0 <= unsigned x < 4294967296 ->
unsigned x mod 4294967296 = unsigned x
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0
        assert (0 <= unsigned x < 4294967296).
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x mod 4294967296 <
2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H1:0 <= unsigned x < 4294967296 ->
unsigned x mod 4294967296 = unsigned x
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x mod 4294967296 <
2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H1:0 <= unsigned x < 4294967296 ->
unsigned x mod 4294967296 = unsigned x
H2:0 <= unsigned x < 4294967296
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0
        pose proof (unsigned_range_2 x).
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x mod 4294967296 <
2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H1:0 <= unsigned x < 4294967296 ->
unsigned x mod 4294967296 = unsigned x
H2:0 <= unsigned x <= max_unsigned
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x mod 4294967296 <
2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H1:0 <= unsigned x < 4294967296 ->
unsigned x mod 4294967296 = unsigned x
H2:0 <= unsigned x < 4294967296
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0 lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x mod 4294967296 <
2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H1:0 <= unsigned x < 4294967296 ->
unsigned x mod 4294967296 = unsigned x
H2:0 <= unsigned x < 4294967296
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0
        apply H1 in H2.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x mod 4294967296 <
2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H1:0 <= unsigned x < 4294967296 ->
unsigned x mod 4294967296 = unsigned x
H2:unsigned x mod 4294967296 = unsigned x
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0 rewrite H2 in l.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:4294967296 - unsigned x < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H1:0 <= unsigned x < 4294967296 ->
unsigned x mod 4294967296 = unsigned x
H2:unsigned x mod 4294967296 = unsigned x
- unsigned x mod 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0 lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x mod 4294967296 <> 0
        rewrite Z.mod_small.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
unsigned x <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
0 <= unsigned x < 4294967296 assumption.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
0 <= unsigned x < 4294967296
        pose proof (unsigned_range_2 x).
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
l0:unsigned x < 2147483648
n:unsigned x <> 0
H:4294967296 <> 0 ->
unsigned x mod 4294967296 <> 0 ->
- unsigned x mod 4294967296 =
4294967296 - unsigned x mod 4294967296
H0:4294967296 <> 0
H1:0 <= unsigned x <= max_unsigned
0 <= unsigned x < 4294967296 lia.
    -
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
- unsigned x mod 4294967296 =
- (unsigned x - 4294967296) destruct (Z.eq_dec (unsigned x) 0).
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
e:unsigned x = 0
- unsigned x mod 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 =
- (unsigned x - 4294967296)
      +
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
e:unsigned x = 0
- unsigned x mod 4294967296 =
- (unsigned x - 4294967296) lia.
      +
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 =
- (unsigned x - 4294967296) rewrite Z.mod_opp_l_nz; try lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
4294967296 - unsigned x mod 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
        rewrite Z.opp_sub_distr.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
4294967296 - unsigned x mod 4294967296 =
- unsigned x + 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
        rewrite Z.mod_small.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
4294967296 - unsigned x = - unsigned x + 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0 lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
        pose proof (unsigned_range_2 x).
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
H:0 <= unsigned x <= max_unsigned
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
        simplify; lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
        rewrite Z.mod_small.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296 assumption.
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
        pose proof (unsigned_range_2 x).
x:Integers.int
Hhalf:unsigned x <> 2147483648
l:- unsigned x mod 4294967296 < 2147483648
g:unsigned x >= 2147483648
n:unsigned x <> 0
H:0 <= unsigned x <= max_unsigned
0 <= unsigned x < 4294967296
        simplify; lia.
    -
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
- unsigned x mod 4294967296 - 4294967296 =
- unsigned x destruct (Z.eq_dec (unsigned x) 0).
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
e:unsigned x = 0
- unsigned x mod 4294967296 - 4294967296 =
- unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 - 4294967296 =
- unsigned x
      +
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
e:unsigned x = 0
- unsigned x mod 4294967296 - 4294967296 =
- unsigned x rewrite e in *.
x:Integers.int
Hhalf:0 <> 2147483648
g:- 0 mod 4294967296 >= 2147483648
l:0 < 2147483648
e:unsigned x = 0
- 0 mod 4294967296 - 4294967296 = - 0 rewrite Z.opp_0 in *.
x:Integers.int
Hhalf:0 <> 2147483648
g:0 mod 4294967296 >= 2147483648
l:0 < 2147483648
e:unsigned x = 0
0 mod 4294967296 - 4294967296 = 0 rewrite Zmod_0_l in g.
x:Integers.int
Hhalf:0 <> 2147483648
g:0 >= 2147483648
l:0 < 2147483648
e:unsigned x = 0
0 mod 4294967296 - 4294967296 = 0 lia.
      +
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 - 4294967296 =
- unsigned x rewrite Z.mod_opp_l_nz; try lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
4294967296 - unsigned x mod 4294967296 - 4294967296 =
- unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
        rewrite Z.mod_small.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
4294967296 - unsigned x - 4294967296 = - unsigned x
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0 lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
        pose proof (unsigned_range_2 x).
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
H:0 <= unsigned x <= max_unsigned
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0 lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
        rewrite Z.mod_small.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
unsigned x <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296 assumption.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
        pose proof (unsigned_range_2 x).
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
l:unsigned x < 2147483648
n:unsigned x <> 0
H:0 <= unsigned x <= max_unsigned
0 <= unsigned x < 4294967296 lia.
    -
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296) destruct (Z.eq_dec (unsigned x) 0).
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
e:unsigned x = 0
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296)
      +
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
e:unsigned x = 0
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296) lia.
      +
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296) rewrite Z.mod_opp_l_nz in g; try lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:4294967296 - unsigned x mod 4294967296 >=
2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
        rewrite Z.mod_small in g.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:4294967296 - unsigned x >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:4294967296 - unsigned x mod 4294967296 >=
2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
        assert (unsigned x < 2147483648) by lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:4294967296 - unsigned x >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
H:unsigned x < 2147483648
- unsigned x mod 4294967296 - 4294967296 =
- (unsigned x - 4294967296)
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:4294967296 - unsigned x mod 4294967296 >=
2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0 lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:4294967296 - unsigned x mod 4294967296 >=
2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
        pose proof (unsigned_range_2 x).
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:4294967296 - unsigned x mod 4294967296 >=
2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
H:0 <= unsigned x <= max_unsigned
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
        replace max_unsigned with 4294967295 in * by auto.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:4294967296 - unsigned x mod 4294967296 >=
2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
H:0 <= unsigned x <= 4294967295
0 <= unsigned x < 4294967296
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0 lia.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x mod 4294967296 <> 0
        rewrite Z.mod_small.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
unsigned x <> 0
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296 assumption.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
0 <= unsigned x < 4294967296
        pose proof (unsigned_range_2 x).
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
H:0 <= unsigned x <= max_unsigned
0 <= unsigned x < 4294967296
        replace max_unsigned with 4294967295 in * by auto.
x:Integers.int
Hhalf:unsigned x <> 2147483648
g:- unsigned x mod 4294967296 >= 2147483648
g0:unsigned x >= 2147483648
n:unsigned x <> 0
H:0 <= unsigned x <= 4294967295
0 <= unsigned x < 4294967296 lia.
  Qed.

  Lemma neg_divs_distr_l :
    forall x y,
      unsigned x <> 2147483648 ->
      neg (divs x y) = divs (neg x) y.
forall x y : Integers.int,
unsigned x <> 2147483648 ->
neg (divs x y) = divs (neg x) y
  Proof.
forall x y : Integers.int,
unsigned x <> 2147483648 ->
neg (divs x y) = divs (neg x) y
    intros x y Hhalf.
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
neg (divs x y) = divs (neg x) y unfold divs, neg.
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
repr (- unsigned (repr (signed x ÷ signed y))) =
repr (signed (repr (- unsigned x)) ÷ signed y)
    set (x' := signed x).
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
x':=signed x:Z
repr (- unsigned (repr (x' ÷ signed y))) =
repr (signed (repr (- unsigned x)) ÷ signed y) set (y' := signed y).
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
x':=signed x:Z
y':=signed y:Z
repr (- unsigned (repr (x' ÷ y'))) =
repr (signed (repr (- unsigned x)) ÷ y')
    apply eqm_samerepr.
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
x':=signed x:Z
y':=signed y:Z
eqm (- unsigned (repr (x' ÷ y')))
  (signed (repr (- unsigned x)) ÷ y')
    apply eqm_trans with (- (Z.quot x' y')).
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
x':=signed x:Z
y':=signed y:Z
eqm (- unsigned (repr (x' ÷ y'))) (- (x' ÷ y'))
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
x':=signed x:Z
y':=signed y:Z
eqm (- (x' ÷ y')) (signed (repr (- unsigned x)) ÷ y')
    auto with ints.
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
x':=signed x:Z
y':=signed y:Z
eqm (- (x' ÷ y')) (signed (repr (- unsigned x)) ÷ y')
    replace (- (Z.quot x' y')) with (Z.quot (- x') y')
      by (rewrite Zquot.Zquot_opp_l; auto).
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
x':=signed x:Z
y':=signed y:Z
eqm (- x' ÷ y') (signed (repr (- unsigned x)) ÷ y')
    unfold x'.
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
x':=signed x:Z
y':=signed y:Z
eqm (- signed x ÷ y')
  (signed (repr (- unsigned x)) ÷ y')
    rewrite <- neg_signed'.
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
x':=signed x:Z
y':=signed y:Z
eqm (signed (neg x) ÷ y')
  (signed (repr (- unsigned x)) ÷ y')
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
x':=signed x:Z
y':=signed y:Z
unsigned x <> 2147483648
    auto with ints.
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
x':=signed x:Z
y':=signed y:Z
unsigned x <> 2147483648
    assumption.
  Qed.

  Lemma neg_signed :
    forall x : int,
      unsigned x <> 2147483648 ->
      signed x < 0 ->
      signed (neg x) >= 0.
forall x : Integers.int,
unsigned x <> 2147483648 ->
signed x < 0 -> signed (neg x) >= 0
  Proof.
forall x : Integers.int,
unsigned x <> 2147483648 ->
signed x < 0 -> signed (neg x) >= 0
    intros.
x:Integers.int
H:unsigned x <> 2147483648
H0:signed x < 0
signed (neg x) >= 0
    rewrite neg_signed'.
x:Integers.int
H:unsigned x <> 2147483648
H0:signed x < 0
- signed x >= 0
x:Integers.int
H:unsigned x <> 2147483648
H0:signed x < 0
unsigned x <> 2147483648 lia.
x:Integers.int
H:unsigned x <> 2147483648
H0:signed x < 0
unsigned x <> 2147483648
    assumption.
  Qed.

  Lemma shl_signed_positive :
    forall y,
      unsigned y <= 30 ->
      signed (shl one y) >= 0.
forall y : Integers.int,
unsigned y <= 30 -> signed (shl one y) >= 0
  Proof.
forall y : Integers.int,
unsigned y <= 30 -> signed (shl one y) >= 0
    intros.
y:Integers.int
H:unsigned y <= 30
signed (shl one y) >= 0
    unfold signed, shl.
y:Integers.int
H:unsigned y <= 30
(if
  zlt
    (unsigned
       (repr (Z.shiftl (unsigned one) (unsigned y))))
    half_modulus
 then
  unsigned
    (repr (Z.shiftl (unsigned one) (unsigned y)))
 else
  unsigned
    (repr (Z.shiftl (unsigned one) (unsigned y))) -
  modulus) >= 0
    destruct (zlt (unsigned (repr (Z.shiftl (unsigned one) (unsigned y)))) half_modulus).
y:Integers.int
H:unsigned y <= 30
l:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) <
half_modulus
unsigned (repr (Z.shiftl (unsigned one) (unsigned y))) >=
0
y:Integers.int
H:unsigned y <= 30
g:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) >=
half_modulus
unsigned (repr (Z.shiftl (unsigned one) (unsigned y))) -
modulus >= 0
    -
y:Integers.int
H:unsigned y <= 30
l:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) <
half_modulus
unsigned (repr (Z.shiftl (unsigned one) (unsigned y))) >=
0 rewrite unsigned_repr.
y:Integers.int
H:unsigned y <= 30
l:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) <
half_modulus
Z.shiftl (unsigned one) (unsigned y) >= 0
y:Integers.int
H:unsigned y <= 30
l:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) <
half_modulus
0 <= Z.shiftl (unsigned one) (unsigned y) <=
max_unsigned
      +
y:Integers.int
H:unsigned y <= 30
l:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) <
half_modulus
Z.shiftl (unsigned one) (unsigned y) >= 0 rewrite Z.shiftl_1_l.
y:Integers.int
H:unsigned y <= 30
l:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) <
half_modulus
2 ^ unsigned y >= 0
        apply Z.le_ge.
y:Integers.int
H:unsigned y <= 30
l:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) <
half_modulus
0 <= 2 ^ unsigned y apply Z.pow_nonneg.
y:Integers.int
H:unsigned y <= 30
l:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) <
half_modulus
0 <= 2 lia.
      +
y:Integers.int
H:unsigned y <= 30
l:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) <
half_modulus
0 <= Z.shiftl (unsigned one) (unsigned y) <=
max_unsigned rewrite Z.shiftl_1_l.
y:Integers.int
H:unsigned y <= 30
l:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) <
half_modulus
0 <= 2 ^ unsigned y <= max_unsigned split.
y:Integers.int
H:unsigned y <= 30
l:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) <
half_modulus
0 <= 2 ^ unsigned y
y:Integers.int
H:unsigned y <= 30
l:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) <
half_modulus
2 ^ unsigned y <= max_unsigned
        apply Z.pow_nonneg.
y:Integers.int
H:unsigned y <= 30
l:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) <
half_modulus
0 <= 2
y:Integers.int
H:unsigned y <= 30
l:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) <
half_modulus
2 ^ unsigned y <= max_unsigned lia.
y:Integers.int
H:unsigned y <= 30
l:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) <
half_modulus
2 ^ unsigned y <= max_unsigned
        simplify.
y:Integers.int
H:unsigned y <= 30
l:Z_mod_modulus (Z.shiftl 1 (unsigned y)) <
half_modulus
2 ^ unsigned y <= 4294967295
        replace (4294967295) with (2 ^ 32 - 1); try lia.
y:Integers.int
H:unsigned y <= 30
l:Z_mod_modulus (Z.shiftl 1 (unsigned y)) <
half_modulus
2 ^ unsigned y <= 2 ^ 32 - 1
        transitivity (2 ^ 31); try lia.
y:Integers.int
H:unsigned y <= 30
l:Z_mod_modulus (Z.shiftl 1 (unsigned y)) <
half_modulus
2 ^ unsigned y <= 2 ^ 31
        apply Z.pow_le_mono_r; lia.
    -
y:Integers.int
H:unsigned y <= 30
g:unsigned
  (repr (Z.shiftl (unsigned one) (unsigned y))) >=
half_modulus
unsigned (repr (Z.shiftl (unsigned one) (unsigned y))) -
modulus >= 0 simplify.
y:Integers.int
H:unsigned y <= 30
g:Z_mod_modulus (Z.shiftl 1 (unsigned y)) >=
half_modulus
Z_mod_modulus (Z.shiftl 1 (unsigned y)) - 4294967296 >=
0 rewrite Z.shiftl_1_l in g.
y:Integers.int
H:unsigned y <= 30
g:Z_mod_modulus (2 ^ unsigned y) >= half_modulus
Z_mod_modulus (Z.shiftl 1 (unsigned y)) - 4294967296 >=
0
      unfold half_modulus, modulus, wordsize,
      Wordsize_32.wordsize in *.
y:Integers.int
H:unsigned y <= 30
g:Z_mod_modulus (2 ^ unsigned y) >=
two_power_nat 32 / 2
Z_mod_modulus (Z.shiftl 1 (unsigned y)) - 4294967296 >=
0 unfold two_power_nat in *.
y:Integers.int
H:unsigned y <= 30
g:Z_mod_modulus (2 ^ unsigned y) >=
Z.pos (shift_nat 32 1) / 2
Z_mod_modulus (Z.shiftl 1 (unsigned y)) - 4294967296 >=
0 simplify.
y:Integers.int
H:unsigned y <= 30
g:Z_mod_modulus (2 ^ unsigned y) >= 4294967296 / 2
Z_mod_modulus (Z.shiftl 1 (unsigned y)) - 4294967296 >=
0
      unfold Z_mod_modulus in *.
y:Integers.int
H:unsigned y <= 30
g:match 2 ^ unsigned y with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end >= 4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      destruct (2 ^ unsigned y) eqn:?.
y:Integers.int
H:unsigned y <= 30
Heqz:2 ^ unsigned y = 0
g:0 >= 4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Zbits.P_mod_two_p p wordsize >= 4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      apply Z.ge_le in g.
y:Integers.int
H:unsigned y <= 30
Heqz:2 ^ unsigned y = 0
g:4294967296 / 2 <= 0
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Zbits.P_mod_two_p p wordsize >= 4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0 exfalso.
y:Integers.int
H:unsigned y <= 30
Heqz:2 ^ unsigned y = 0
g:4294967296 / 2 <= 0
False
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Zbits.P_mod_two_p p wordsize >= 4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      replace (4294967296 / 2) with (2147483648) in g; auto.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Zbits.P_mod_two_p p wordsize >= 4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      rewrite Z.shiftl_1_l.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Zbits.P_mod_two_p p wordsize >= 4294967296 / 2
match 2 ^ unsigned y with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0 rewrite Heqz.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Zbits.P_mod_two_p p wordsize >= 4294967296 / 2
Zbits.P_mod_two_p p wordsize - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      unfold wordsize in *.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Zbits.P_mod_two_p p Wordsize_32.wordsize >=
4294967296 / 2
Zbits.P_mod_two_p p Wordsize_32.wordsize - 4294967296 >=
0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0 unfold Wordsize_32.wordsize in *.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Zbits.P_mod_two_p p 32 >= 4294967296 / 2
Zbits.P_mod_two_p p 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      rewrite Zbits.P_mod_two_p_eq in *.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Z.pos p mod two_power_nat 32 >= 4294967296 / 2
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      replace (4294967296 / 2) with (2147483648) in g; auto.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:Z.pos p mod two_power_nat 32 >= 2147483648
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      rewrite <- Heqz in g.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      rewrite Z.mod_small in g.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2147483648
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      replace (2147483648) with (2 ^ 31) in g.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2 ^ 31
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2147483648
2 ^ 31 = 2147483648
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      pose proof (Z.pow_le_mono_r 2 (unsigned y) 30).
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2 ^ 31
H0:0 < 2 ->
unsigned y <= 30 -> 2 ^ unsigned y <= 2 ^ 30
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2147483648
2 ^ 31 = 2147483648
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      apply Z.ge_le in g.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ 31 <= 2 ^ unsigned y
H0:0 < 2 ->
unsigned y <= 30 -> 2 ^ unsigned y <= 2 ^ 30
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2147483648
2 ^ 31 = 2147483648
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      assert (0 < 2) by lia.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ 31 <= 2 ^ unsigned y
H0:0 < 2 ->
unsigned y <= 30 -> 2 ^ unsigned y <= 2 ^ 30
H1:0 < 2
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2147483648
2 ^ 31 = 2147483648
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0 apply H0 in H1.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ 31 <= 2 ^ unsigned y
H0:0 < 2 ->
unsigned y <= 30 -> 2 ^ unsigned y <= 2 ^ 30
H1:2 ^ unsigned y <= 2 ^ 30
Z.pos p mod two_power_nat 32 - 4294967296 >= 0
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ 31 <= 2 ^ unsigned y
H0:0 < 2 ->
unsigned y <= 30 -> 2 ^ unsigned y <= 2 ^ 30
H1:0 < 2
unsigned y <= 30
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2147483648
2 ^ 31 = 2147483648
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0 lia.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ 31 <= 2 ^ unsigned y
H0:0 < 2 ->
unsigned y <= 30 -> 2 ^ unsigned y <= 2 ^ 30
H1:0 < 2
unsigned y <= 30
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2147483648
2 ^ 31 = 2147483648
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0 assumption.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y >= 2147483648
2 ^ 31 = 2147483648
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0 lia.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      split.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
0 <= 2 ^ unsigned y
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0 lia.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
2 ^ unsigned y < two_power_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0 rewrite two_power_nat_equiv.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.pos p
g:2 ^ unsigned y mod two_power_nat 32 >= 2147483648
2 ^ unsigned y < 2 ^ Z.of_nat 32
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      apply Z.pow_lt_mono_r; lia.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0

      pose proof (Zlt_neg_0 p).
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
H0:Z.neg p < 0
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      pose proof (Z.pow_nonneg 2 (unsigned y)).
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
H0:Z.neg p < 0
H1:0 <= 2 -> 0 <= 2 ^ unsigned y
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0 rewrite <- Heqz in H0.
y:Integers.int
H:unsigned y <= 30
p:positive
Heqz:2 ^ unsigned y = Z.neg p
g:(if zeq (Zbits.P_mod_two_p p wordsize) 0
 then 0
 else modulus - Zbits.P_mod_two_p p wordsize) >=
4294967296 / 2
H0:2 ^ unsigned y < 0
H1:0 <= 2 -> 0 <= 2 ^ unsigned y
match Z.shiftl 1 (unsigned y) with
| 0 => 0
| Z.pos p => Zbits.P_mod_two_p p wordsize
| Z.neg p =>
    if zeq (Zbits.P_mod_two_p p wordsize) 0
    then 0
    else modulus - Zbits.P_mod_two_p p wordsize
end - 4294967296 >= 0
      lia.
  Qed.

  Lemma is_power2_shl :
    forall y,
      unsigned y <= 30 ->
      is_power2 (shl one y) = Some y.
forall y : Integers.int,
unsigned y <= 30 -> is_power2 (shl one y) = Some y
  Proof.
forall y : Integers.int,
unsigned y <= 30 -> is_power2 (shl one y) = Some y
    intros.
y:Integers.int
H:unsigned y <= 30
is_power2 (shl one y) = Some y
    unfold is_power2, shl.
y:Integers.int
H:unsigned y <= 30
match
  Zbits.Z_is_power2
    (unsigned
       (repr (Z.shiftl (unsigned one) (unsigned y))))
with
| Some i => Some (repr i)
| None => None
end = Some y
    destruct (Zbits.Z_is_power2 (unsigned (repr (Z.shiftl (unsigned one) (unsigned y))))) eqn:?.
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (unsigned
     (repr
        (Z.shiftl (unsigned one) (unsigned y)))) =
Some z
Some (repr z) = Some y
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (unsigned
     (repr
        (Z.shiftl (unsigned one) (unsigned y)))) =
None
None = Some y
    -
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (unsigned
     (repr
        (Z.shiftl (unsigned one) (unsigned y)))) =
Some z
Some (repr z) = Some y simplify.
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z_mod_modulus (Z.shiftl 1 (unsigned y))) =
Some z
repr z = y
      rewrite Z_mod_modulus_eq in Heqo.
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
repr z = y
      rewrite Z.mod_small in Heqo.
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2 (Z.shiftl 1 (unsigned y)) =
Some z
repr z = y
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
0 <= Z.shiftl 1 (unsigned y) < modulus rewrite Z.shiftl_1_l in Heqo.
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2 (2 ^ unsigned y) = Some z
repr z = y
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
0 <= Z.shiftl 1 (unsigned y) < modulus
      rewrite <- two_p_correct in Heqo.
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2 (two_p (unsigned y)) = Some z
repr z = y
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
0 <= Z.shiftl 1 (unsigned y) < modulus
      rewrite Zbits.Z_is_power2_complete in Heqo.
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Some (unsigned y) = Some z
repr z = y
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2 (two_p (unsigned y)) = Some z
0 <= unsigned y
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
0 <= Z.shiftl 1 (unsigned y) < modulus inv Heqo.
y:Integers.int
H:unsigned y <= 30
repr (unsigned y) = y
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2 (two_p (unsigned y)) = Some z
0 <= unsigned y
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
0 <= Z.shiftl 1 (unsigned y) < modulus
      rewrite repr_unsigned.
y:Integers.int
H:unsigned y <= 30
y = y
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2 (two_p (unsigned y)) = Some z
0 <= unsigned y
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
0 <= Z.shiftl 1 (unsigned y) < modulus auto.
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2 (two_p (unsigned y)) = Some z
0 <= unsigned y
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
0 <= Z.shiftl 1 (unsigned y) < modulus
      pose proof (unsigned_range_2 y).
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2 (two_p (unsigned y)) = Some z
H0:0 <= unsigned y <= max_unsigned
0 <= unsigned y
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
0 <= Z.shiftl 1 (unsigned y) < modulus lia.
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
0 <= Z.shiftl 1 (unsigned y) < modulus
      rewrite Z.shiftl_1_l.
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
0 <= 2 ^ unsigned y < modulus unfold modulus, wordsize, Wordsize_32.wordsize.
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
0 <= 2 ^ unsigned y < two_power_nat 32
      rewrite two_power_nat_equiv.
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
0 <= 2 ^ unsigned y < 2 ^ Z.of_nat 32
      split.
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
0 <= 2 ^ unsigned y
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
2 ^ unsigned y < 2 ^ Z.of_nat 32 apply Z.pow_nonneg.
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
0 <= 2
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
2 ^ unsigned y < 2 ^ Z.of_nat 32 lia.
y:Integers.int
H:unsigned y <= 30
z:Z
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) =
Some z
2 ^ unsigned y < 2 ^ Z.of_nat 32
      apply Z.pow_lt_mono_r; lia.
    -
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (unsigned
     (repr
        (Z.shiftl (unsigned one) (unsigned y)))) =
None
None = Some y simplify.
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z_mod_modulus (Z.shiftl 1 (unsigned y))) =
None
None = Some y
      rewrite Z_mod_modulus_eq in Heqo.
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) = None
None = Some y
      rewrite Z.mod_small in Heqo.
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2 (Z.shiftl 1 (unsigned y)) =
None
None = Some y
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) = None
0 <= Z.shiftl 1 (unsigned y) < modulus rewrite Z.shiftl_1_l in Heqo.
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2 (2 ^ unsigned y) = None
None = Some y
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) = None
0 <= Z.shiftl 1 (unsigned y) < modulus
      rewrite <- two_p_correct in Heqo.
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2 (two_p (unsigned y)) = None
None = Some y
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) = None
0 <= Z.shiftl 1 (unsigned y) < modulus
      rewrite Zbits.Z_is_power2_complete in Heqo.
y:Integers.int
H:unsigned y <= 30
Heqo:Some (unsigned y) = None
None = Some y
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2 (two_p (unsigned y)) = None
0 <= unsigned y
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) = None
0 <= Z.shiftl 1 (unsigned y) < modulus discriminate.
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2 (two_p (unsigned y)) = None
0 <= unsigned y
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) = None
0 <= Z.shiftl 1 (unsigned y) < modulus
      pose proof (unsigned_range_2 y).
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2 (two_p (unsigned y)) = None
H0:0 <= unsigned y <= max_unsigned
0 <= unsigned y
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) = None
0 <= Z.shiftl 1 (unsigned y) < modulus lia.
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) = None
0 <= Z.shiftl 1 (unsigned y) < modulus
      rewrite Z.shiftl_1_l.
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) = None
0 <= 2 ^ unsigned y < modulus unfold modulus, wordsize, Wordsize_32.wordsize.
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) = None
0 <= 2 ^ unsigned y < two_power_nat 32
      rewrite two_power_nat_equiv.
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) = None
0 <= 2 ^ unsigned y < 2 ^ Z.of_nat 32
      split.
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) = None
0 <= 2 ^ unsigned y
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) = None
2 ^ unsigned y < 2 ^ Z.of_nat 32 apply Z.pow_nonneg.
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) = None
0 <= 2
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) = None
2 ^ unsigned y < 2 ^ Z.of_nat 32 lia.
y:Integers.int
H:unsigned y <= 30
Heqo:Zbits.Z_is_power2
  (Z.shiftl 1 (unsigned y) mod modulus) = None
2 ^ unsigned y < 2 ^ Z.of_nat 32
      apply Z.pow_lt_mono_r; lia.
  Qed.

  Definition shrx_alt (x y : int) : int :=
    if zlt (signed x) 0
    then neg (shru (neg x) y)
    else shru x y.

  Lemma shrx_shrx_alt_equiv_ne :
    forall x y,
      unsigned x <> 2147483648 ->
      unsigned y <= 30 ->
      shrx x y = shrx_alt x y.
forall x y : Integers.int,
unsigned x <> 2147483648 ->
unsigned y <= 30 -> shrx x y = shrx_alt x y
  Proof.
forall x y : Integers.int,
unsigned x <> 2147483648 ->
unsigned y <= 30 -> shrx x y = shrx_alt x y
    intros x y Hhalf H.
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
H:unsigned y <= 30
shrx x y = shrx_alt x y
    unfold shrx, shrx_alt, lt.
x, y:Integers.int
Hhalf:unsigned x <> 2147483648
H:unsigned y <= 30
divs x (shl one y) =
(if zlt (signed x) 0
 then neg (shru (neg x) y)
 else shru x y)
    destruct (Z_ge_lt_dec (signed x) 0);
      [rewrite zlt_false | rewrite zlt_true];

      repeat lazymatch goal with
             | |- is_power2 _ = Some _ => apply is_power2_shl
             | |- signed (shl one _) >= 0 => apply shl_signed_positive
             | |- signed (neg _) >= 0 => apply neg_signed
             | |- divs _ _ = divu _ _ => apply div_divs_equiv
             | |- divs ?x (shl one ?y) = neg (shru (neg ?x) ?y) =>
               rewrite <- neg_involutive at 1; rewrite neg_divs_distr_l;
                 try assumption; f_equal
             | |- divs ?x (shl one ?y) = shru ?x ?y =>
               let H := fresh "H" in
               pose proof (divu_pow2 x (shl one y) y) as H;
                 rewrite <- H
             end; try assumption.
  Qed.

  Lemma shrx_shrx_alt_equiv_eq :
    forall x y,
      unsigned x = 2147483648 ->
      unsigned y <= 30 ->
      shrx x y = shrx_alt x y.
forall x y : Integers.int,
unsigned x = 2147483648 ->
unsigned y <= 30 -> shrx x y = shrx_alt x y
  Proof.
forall x y : Integers.int,
unsigned x = 2147483648 ->
unsigned y <= 30 -> shrx x y = shrx_alt x y
    intros.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
shrx x y = shrx_alt x y
    repeat unfold shrx, shrx_alt, signed, divs, neg.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
repr
  ((if zlt (unsigned x) half_modulus
    then unsigned x
    else unsigned x - modulus)
   ÷ (if zlt (unsigned (shl one y)) half_modulus
      then unsigned (shl one y)
      else unsigned (shl one y) - modulus)) =
(if
  zlt
    (if zlt (unsigned x) half_modulus
     then unsigned x
     else unsigned x - modulus) 0
 then repr (- unsigned (shru (repr (- unsigned x)) y))
 else shru x y)
    replace half_modulus with 2147483648 by auto.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
repr
  ((if zlt (unsigned x) 2147483648
    then unsigned x
    else unsigned x - modulus)
   ÷ (if zlt (unsigned (shl one y)) 2147483648
      then unsigned (shl one y)
      else unsigned (shl one y) - modulus)) =
(if
  zlt
    (if zlt (unsigned x) 2147483648
     then unsigned x
     else unsigned x - modulus) 0
 then repr (- unsigned (shru (repr (- unsigned x)) y))
 else shru x y)
    replace modulus with 4294967296 by auto.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
repr
  ((if zlt (unsigned x) 2147483648
    then unsigned x
    else unsigned x - 4294967296)
   ÷ (if zlt (unsigned (shl one y)) 2147483648
      then unsigned (shl one y)
      else unsigned (shl one y) - 4294967296)) =
(if
  zlt
    (if zlt (unsigned x) 2147483648
     then unsigned x
     else unsigned x - 4294967296) 0
 then repr (- unsigned (shru (repr (- unsigned x)) y))
 else shru x y)
    simplify.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
repr
  ((if zlt (unsigned x) 2147483648
    then unsigned x
    else unsigned x - 4294967296)
   ÷ (if
       zlt (Z_mod_modulus (Z.shiftl 1 (unsigned y)))
         2147483648
      then Z_mod_modulus (Z.shiftl 1 (unsigned y))
      else
       Z_mod_modulus (Z.shiftl 1 (unsigned y)) -
       4294967296)) =
(if
  zlt
    (if zlt (unsigned x) 2147483648
     then unsigned x
     else unsigned x - 4294967296) 0
 then
  repr
    (-
     Z_mod_modulus
       (Z.shiftr (Z_mod_modulus (- unsigned x))
          (unsigned y)))
 else shru x y)
    rewrite !Z_mod_modulus_eq.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
repr
  ((if zlt (unsigned x) 2147483648
    then unsigned x
    else unsigned x - 4294967296)
   ÷ (if
       zlt (Z.shiftl 1 (unsigned y) mod modulus)
         2147483648
      then Z.shiftl 1 (unsigned y) mod modulus
      else
       Z.shiftl 1 (unsigned y) mod modulus -
       4294967296)) =
(if
  zlt
    (if zlt (unsigned x) 2147483648
     then unsigned x
     else unsigned x - 4294967296) 0
 then
  repr
    (-
     (Z.shiftr (- unsigned x mod modulus) (unsigned y)
      mod modulus))
 else shru x y)
    rewrite !H.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
repr
  ((if zlt 2147483648 2147483648
    then 2147483648
    else 2147483648 - 4294967296)
   ÷ (if
       zlt (Z.shiftl 1 (unsigned y) mod modulus)
         2147483648
      then Z.shiftl 1 (unsigned y) mod modulus
      else
       Z.shiftl 1 (unsigned y) mod modulus -
       4294967296)) =
(if
  zlt
    (if zlt 2147483648 2147483648
     then 2147483648
     else 2147483648 - 4294967296) 0
 then
  repr
    (-
     (Z.shiftr (- (2147483648) mod modulus)
        (unsigned y) mod modulus))
 else shru x y)
    simplify.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
repr
  (-2147483648
   ÷ (if
       zlt (Z.shiftl 1 (unsigned y) mod 4294967296)
         2147483648
      then Z.shiftl 1 (unsigned y) mod 4294967296
      else
       Z.shiftl 1 (unsigned y) mod 4294967296 -
       4294967296)) =
repr
  (-
   (Z.shiftr (-2147483648 mod 4294967296) (unsigned y)
    mod 4294967296))
    assert (Hshl: Z.shiftl 1 (unsigned y) mod 4294967296 = Z.shiftl 1 (unsigned y)).
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
repr
  (-2147483648
   ÷ (if
       zlt (Z.shiftl 1 (unsigned y) mod 4294967296)
         2147483648
      then Z.shiftl 1 (unsigned y) mod 4294967296
      else
       Z.shiftl 1 (unsigned y) mod 4294967296 -
       4294967296)) =
repr
  (-
   (Z.shiftr (-2147483648 mod 4294967296) (unsigned y)
    mod 4294967296))
    {
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y) apply Z.mod_small.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
0 <= Z.shiftl 1 (unsigned y) < 4294967296
      rewrite Z.shiftl_1_l.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
0 <= 2 ^ unsigned y < 4294967296
      split.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
0 <= 2 ^ unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
2 ^ unsigned y < 4294967296
      apply Z.pow_nonneg.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
0 <= 2
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
2 ^ unsigned y < 4294967296 lia.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
2 ^ unsigned y < 4294967296
      replace 4294967296 with (2^32) by auto.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
2 ^ unsigned y < 2 ^ 32
      apply Z.le_lt_trans with (m := 2 ^ 31); try lia.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
2 ^ unsigned y <= 2 ^ 31
      apply Z.pow_le_mono_r; lia.
    }
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
repr
  (-2147483648
   ÷ (if
       zlt (Z.shiftl 1 (unsigned y) mod 4294967296)
         2147483648
      then Z.shiftl 1 (unsigned y) mod 4294967296
      else
       Z.shiftl 1 (unsigned y) mod 4294967296 -
       4294967296)) =
repr
  (-
   (Z.shiftr (-2147483648 mod 4294967296) (unsigned y)
    mod 4294967296))
    rewrite !Hshl.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
repr
  (-2147483648
   ÷ (if zlt (Z.shiftl 1 (unsigned y)) 2147483648
      then Z.shiftl 1 (unsigned y)
      else Z.shiftl 1 (unsigned y) - 4294967296)) =
repr
  (-
   (Z.shiftr (-2147483648 mod 4294967296) (unsigned y)
    mod 4294967296))
    f_equal.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
-2147483648
÷ (if zlt (Z.shiftl 1 (unsigned y)) 2147483648
   then Z.shiftl 1 (unsigned y)
   else Z.shiftl 1 (unsigned y) - 4294967296) =
-
(Z.shiftr (-2147483648 mod 4294967296) (unsigned y)
 mod 4294967296)
    assert ((Z.shiftl 1 (unsigned y)) < 2147483648).
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
Z.shiftl 1 (unsigned y) < 2147483648
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1:Z.shiftl 1 (unsigned y) < 2147483648
-2147483648
÷ (if zlt (Z.shiftl 1 (unsigned y)) 2147483648
   then Z.shiftl 1 (unsigned y)
   else Z.shiftl 1 (unsigned y) - 4294967296) =
-
(Z.shiftr (-2147483648 mod 4294967296) (unsigned y)
 mod 4294967296)
    rewrite Z.shiftl_1_l.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
2 ^ unsigned y < 2147483648
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1:Z.shiftl 1 (unsigned y) < 2147483648
-2147483648
÷ (if zlt (Z.shiftl 1 (unsigned y)) 2147483648
   then Z.shiftl 1 (unsigned y)
   else Z.shiftl 1 (unsigned y) - 4294967296) =
-
(Z.shiftr (-2147483648 mod 4294967296) (unsigned y)
 mod 4294967296)
    replace 2147483648 with (2^31) by auto.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
2 ^ unsigned y < 2 ^ 31
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1:Z.shiftl 1 (unsigned y) < 2147483648
-2147483648
÷ (if zlt (Z.shiftl 1 (unsigned y)) 2147483648
   then Z.shiftl 1 (unsigned y)
   else Z.shiftl 1 (unsigned y) - 4294967296) =
-
(Z.shiftr (-2147483648 mod 4294967296) (unsigned y)
 mod 4294967296)
    apply Z.le_lt_trans with (m := 2 ^ 30); try lia.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
2 ^ unsigned y <= 2 ^ 30
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1:Z.shiftl 1 (unsigned y) < 2147483648
-2147483648
÷ (if zlt (Z.shiftl 1 (unsigned y)) 2147483648
   then Z.shiftl 1 (unsigned y)
   else Z.shiftl 1 (unsigned y) - 4294967296) =
-
(Z.shiftr (-2147483648 mod 4294967296) (unsigned y)
 mod 4294967296)
    apply Z.pow_le_mono_r; lia.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1:Z.shiftl 1 (unsigned y) < 2147483648
-2147483648
÷ (if zlt (Z.shiftl 1 (unsigned y)) 2147483648
   then Z.shiftl 1 (unsigned y)
   else Z.shiftl 1 (unsigned y) - 4294967296) =
-
(Z.shiftr (-2147483648 mod 4294967296) (unsigned y)
 mod 4294967296)
    destruct (zlt (Z.shiftl 1 (unsigned y)) 2147483648); try lia.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
-2147483648 ÷ Z.shiftl 1 (unsigned y) =
-
(Z.shiftr (-2147483648 mod 4294967296) (unsigned y)
 mod 4294967296)
    replace (-2147483648 mod 4294967296) with 2147483648 by auto.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
-2147483648 ÷ Z.shiftl 1 (unsigned y) =
- (Z.shiftr 2147483648 (unsigned y) mod 4294967296)
    assert (Hmodeq : Z.shiftr 2147483648 (unsigned y) mod 4294967296
                     = Z.shiftr 2147483648 (unsigned y)).
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Z.shiftr 2147483648 (unsigned y) mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
-2147483648 ÷ Z.shiftl 1 (unsigned y) =
- (Z.shiftr 2147483648 (unsigned y) mod 4294967296)
    {
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Z.shiftr 2147483648 (unsigned y) mod 4294967296 =
Z.shiftr 2147483648 (unsigned y) apply Z.mod_small.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= Z.shiftr 2147483648 (unsigned y) < 4294967296 split.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= Z.shiftr 2147483648 (unsigned y)
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Z.shiftr 2147483648 (unsigned y) < 4294967296
      apply Z.shiftr_nonneg.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= 2147483648
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Z.shiftr 2147483648 (unsigned y) < 4294967296 lia.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Z.shiftr 2147483648 (unsigned y) < 4294967296
      rewrite Z.shiftr_div_pow2.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
2147483648 / 2 ^ unsigned y < 4294967296
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y
      replace 4294967296 with (Z.succ 4294967295); auto.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
2147483648 / 2 ^ unsigned y < Z.succ 4294967295
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y
      apply Zle_lt_succ.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
2147483648 / 2 ^ unsigned y <= 4294967295
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y
      replace 4294967295 with (4294967295 * (2 ^ unsigned y) / (2 ^ unsigned y)).
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
2147483648 / 2 ^ unsigned y <=
4294967295 * 2 ^ unsigned y / 2 ^ unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
4294967295 * 2 ^ unsigned y / 2 ^ unsigned y =
4294967295
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y
      2: {
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
4294967295 * 2 ^ unsigned y / 2 ^ unsigned y =
4294967295
          apply Z.div_mul.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
2 ^ unsigned y <> 0
          pose proof (Z.pow_pos_nonneg 2 (unsigned y)).
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
H2:0 < 2 -> 0 <= unsigned y -> 0 < 2 ^ unsigned y
2 ^ unsigned y <> 0
          apply not_eq_sym.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
H2:0 < 2 -> 0 <= unsigned y -> 0 < 2 ^ unsigned y
0 <> 2 ^ unsigned y
          apply Z.le_neq.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
H2:0 < 2 -> 0 <= unsigned y -> 0 < 2 ^ unsigned y
0 < 2 ^ unsigned y apply H2; try lia.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
H2:0 < 2 -> 0 <= unsigned y -> 0 < 2 ^ unsigned y
0 <= unsigned y
          apply unsigned_range_2.
      }
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
2147483648 / 2 ^ unsigned y <=
4294967295 * 2 ^ unsigned y / 2 ^ unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y

      apply Z.div_le_mono.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 < 2 ^ unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
2147483648 <= 4294967295 * 2 ^ unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y
      apply Z.pow_pos_nonneg.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 < 2
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
2147483648 <= 4294967295 * 2 ^ unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y lia.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
2147483648 <= 4294967295 * 2 ^ unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y
      apply unsigned_range_2.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
2147483648 <= 4294967295 * 2 ^ unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y
      transitivity 4294967295; try lia.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
4294967295 <= 4294967295 * 2 ^ unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y
      apply Z.le_mul_diag_r; try lia.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
1 <= 2 ^ unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y
      replace 1 with (Z.succ 0) by auto.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Z.succ 0 <= 2 ^ unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y
      apply Z.le_succ_l.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 < 2 ^ unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y
      apply Z.pow_pos_nonneg; try lia.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y
      apply unsigned_range_2.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
0 <= unsigned y apply unsigned_range_2.
    }
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
-2147483648 ÷ Z.shiftl 1 (unsigned y) =
- (Z.shiftr 2147483648 (unsigned y) mod 4294967296)
    rewrite !Hmodeq.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
-2147483648 ÷ Z.shiftl 1 (unsigned y) =
- Z.shiftr 2147483648 (unsigned y)
    replace (-2147483648) with (Z.opp 2147483648) by auto.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
- (2147483648) ÷ Z.shiftl 1 (unsigned y) =
- Z.shiftr 2147483648 (unsigned y)
    rewrite Zquot.Zquot_opp_l.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
- (2147483648 ÷ Z.shiftl 1 (unsigned y)) =
- Z.shiftr 2147483648 (unsigned y)
    f_equal.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
2147483648 ÷ Z.shiftl 1 (unsigned y) =
Z.shiftr 2147483648 (unsigned y)
    rewrite Zquot.Zquot_Zdiv_pos.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
2147483648 / Z.shiftl 1 (unsigned y) =
Z.shiftr 2147483648 (unsigned y)
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 <= 2147483648
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 <= Z.shiftl 1 (unsigned y)
    rewrite Z.shiftr_div_pow2.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
2147483648 / Z.shiftl 1 (unsigned y) =
2147483648 / 2 ^ unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 <= unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 <= 2147483648
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 <= Z.shiftl 1 (unsigned y)
    rewrite Z.shiftl_1_l.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
2147483648 / 2 ^ unsigned y =
2147483648 / 2 ^ unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 <= unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 <= 2147483648
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 <= Z.shiftl 1 (unsigned y) auto.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 <= unsigned y
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 <= 2147483648
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 <= Z.shiftl 1 (unsigned y)
    apply unsigned_range_2.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 <= 2147483648
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 <= Z.shiftl 1 (unsigned y)
    lia.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 <= Z.shiftl 1 (unsigned y)
    rewrite Z.shiftl_1_l.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 <= 2 ^ unsigned y
    apply Z.lt_le_incl.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 < 2 ^ unsigned y
    apply Z.pow_pos_nonneg; try lia.
x, y:Integers.int
H:unsigned x = 2147483648
H0:unsigned y <= 30
Hshl:Z.shiftl 1 (unsigned y) mod 4294967296 =
Z.shiftl 1 (unsigned y)
H1, l:Z.shiftl 1 (unsigned y) < 2147483648
Hmodeq:Z.shiftr 2147483648 (unsigned y)
mod 4294967296 =
Z.shiftr 2147483648 (unsigned y)
0 <= unsigned y
    apply unsigned_range_2.
  Qed.

  Theorem shrx_shrx_alt_equiv :
    forall x y,
      unsigned y <= 30 ->
      shrx x y = shrx_alt x y.
forall x y : Integers.int,
unsigned y <= 30 -> shrx x y = shrx_alt x y
  Proof.
forall x y : Integers.int,
unsigned y <= 30 -> shrx x y = shrx_alt x y
    intros.
x, y:Integers.int
H:unsigned y <= 30
shrx x y = shrx_alt x y
    destruct (Z.eq_dec (unsigned x) 2147483648);
    [ apply shrx_shrx_alt_equiv_eq | apply shrx_shrx_alt_equiv_ne]; auto.
  Qed.

End IntExtra.