Port the Coq part

6 files changed, 121 insertions, 130 deletions

diff --git a/src/SMT_terms.v b/src/SMT_terms.v
index aa49904..e6c67a2 100644
--- a/src/SMT_terms.v
+++ b/src/SMT_terms.v
@@ -105,7 +105,7 @@ Module Form.
             t_b.[i <- interp_aux (PArray.get t_b) hf])
         (PArray.make (PArray.length t_form) true) t_form.
 
-      Fixpoint lt_form i h {struct h} :=
+      Definition lt_form i h :=
         match h with
         | Fatom _ | Ftrue | Ffalse => true
         | Fnot2 _ l => Lit.blit l < i
diff --git a/src/State.v b/src/State.v
index 663b2b3..4431fbb 100644
--- a/src/State.v
+++ b/src/State.v
@@ -10,7 +10,7 @@
 (**************************************************************************)
 
 
-Require Import List Bool Int63 PArray Omega.
+Require Import List Bool Int63 PArray Psatz.
 
 (* Require Import AxiomesInt. *)
 
@@ -239,7 +239,7 @@ Proof.
   rewrite <- eqb_spec;trivial.
   rewrite <- not_true_iff_false in H, H0.
   unfold is_true in *;rewrite ltb_spec in H |- *;rewrite eqb_spec in H0.
-  assert ([|x|] <> [|y|]) by (intros Heq;apply H0, to_Z_inj;trivial);omega.
+  assert ([|x|] <> [|y|]) by (intros Heq;apply H0, to_Z_inj;trivial);lia.
 Qed.
 
 
@@ -358,7 +358,7 @@ Module C.
       intros rho resolve_correct Hc1;simpl in Hc1.
       induction c2;simpl;try discriminate.
       generalize (compare_spec' l1 a);destruct (l1 ?= a);intros;subst;simpl.
-      simpl in Hc1;destruct (Lit.interp rho a);simpl in *;auto.
+      simpl in Hc1;destruct (Lit.interp rho l1);simpl in *;auto.
       generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros.
       rewrite or_correct.
       rewrite H1, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho a).
diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v
index 71450dc..19fc18e 100644
--- a/src/bva/Bva_checker.v
+++ b/src/bva/Bva_checker.v
@@ -1318,7 +1318,7 @@ Proof. intros a bs.
        induction bs as [ | b ys IHys].
        - intros. simpl in H. 
          cut (i = n). intro Hn. rewrite Hn in H1.
-         contradict H1. omega. omega.
+         contradict H1. lia. lia.
        - intros. simpl in H0.
          case_eq (Lit.is_pos b). intros Heq0. rewrite Heq0 in H0.
          case_eq (t_form .[ Lit.blit b] ). intros i1 Heq1. rewrite Heq1 in H0.
@@ -1349,7 +1349,7 @@ Proof. intros a bs.
          cut ((S k - S i)%nat = (k - i)%nat). intro ISki.
          specialize (@IHys Hd).
          now rewrite ISki in IHys.
-         now simpl. omega.
+         now simpl. lia.
          rewrite Hd.
          cut ((i0 - i0 = 0)%nat). intro Hi0. rewrite Hi0.
          simpl.
@@ -1417,13 +1417,13 @@ Proof. intros a bs.
          now apply Nat_eqb_eq in Hif2.
          now apply Nat_eqb_eq in Hif1.
 
-         omega.
+         lia.
          destruct H1.
          specialize (@le_le_S_eq i i0). intros H11.
          specialize (@H11 H1).
          destruct H11. left. split. exact H5. exact H3.
          right. exact H5.
-         omega.
+         lia.
          intro H3. rewrite H3 in H0. now contradict H0.
          intros n0 Hn. rewrite Hn in H0. now contradict H0.
          intros n0 Hn. rewrite Hn in H0. now contradict H0.
@@ -1464,7 +1464,7 @@ Proof. intros.
        cut ( (0 <= i0 < Datatypes.length bs)%nat). intro Hc3.
        specialize (@Hp Hc3).
        now rewrite Hc in Hp.
-       omega. omega. omega.
+       lia. lia. lia.
 Qed.
 
 
@@ -1501,7 +1501,7 @@ Proof. intros a.
            cut ((0 < S (Datatypes.length xs))%nat). intro HS.
            specialize (@H2 HS). rewrite H2; apply f_equal.
            apply IHxs. intros. apply (@nth_eq0 i a b xs ys).
-           apply H. simpl. omega. omega.
+           apply H. simpl. lia. lia.
 Qed.
 
 Lemma is_even_0: is_even 0 = true.
@@ -1645,7 +1645,7 @@ Proof.
   case (t_form .[ Lit.blit b]) in Hc; try now contradict Hc.
   case a in Hc; try now contradict Hc. exact Hc.
   case a in Hc; try now contradict Hc. exact Hc.
-  simpl in Hlen. omega.
+  simpl in Hlen. lia.
 Qed.
 
 Lemma prop_check_bbc2: forall l bs, check_bbc l bs = true ->
@@ -2890,7 +2890,7 @@ Proof. intros bs1 bs2 bsres.
              specialize (IHbsres bs1 bs2 (n-1)%nat).
              simpl in H0.
              assert (length bs1 = (n-1)%nat).
-             { omega. }
+             { lia. }
 
              cut ( (BO_BVand (N.of_nat n - 1)) = (BO_BVand (N.of_nat (n - 1)))).
 
@@ -2899,7 +2899,7 @@ Proof. intros bs1 bs2 bsres.
              rewrite H2.
              intros.
              specialize (IHbsres H H1).
-             simpl. rewrite IHbsres. omega.
+             simpl. rewrite IHbsres. lia.
 
              simpl.
              cut ((N.of_nat n - 1)%N = (N.of_nat (n - 1))).
@@ -3017,7 +3017,7 @@ Proof. intros bs1 bs2 bsres.
              specialize (IHbsres bs1 bs2 (n-1)%nat).
              simpl in H0.
              assert (length bs1 = (n-1)%nat).
-             { omega. }
+             { lia. }
 
              cut ( (BO_BVor (N.of_nat n - 1)) = (BO_BVor (N.of_nat (n - 1)))).
 
@@ -3026,7 +3026,7 @@ Proof. intros bs1 bs2 bsres.
              rewrite H2.
              intros.
              specialize (IHbsres H H1).
-             simpl. rewrite IHbsres. omega.
+             simpl. rewrite IHbsres. lia.
 
              simpl.
              cut ((N.of_nat n - 1)%N = (N.of_nat (n - 1))).
@@ -3142,7 +3142,7 @@ Proof. intros bs1 bs2 bsres.
              specialize (IHbsres bs1 bs2 (n-1)%nat).
              simpl in H0.
              assert (length bs1 = (n-1)%nat).
-             { omega. }
+             { lia. }
 
              cut ( (BO_BVxor (N.of_nat n - 1)) = (BO_BVxor (N.of_nat (n - 1)))).
 
@@ -3151,7 +3151,7 @@ Proof. intros bs1 bs2 bsres.
              rewrite H2.
              intros.
              specialize (IHbsres H H1).
-             simpl. rewrite IHbsres. omega.
+             simpl. rewrite IHbsres. lia.
 
              simpl.
              cut ((N.of_nat n - 1)%N = (N.of_nat (n - 1))).
@@ -6515,7 +6515,7 @@ Proof. intro a.
        induction a as [ | xa xsa IHa ].
        - intros. simpl. easy.
        - intros.
-         case b in *. simpl. rewrite IHa. simpl. omega.
+         case b in *. simpl. rewrite IHa. simpl. lia.
          simpl. case (k - 1 <? 0)%Z; simpl; now rewrite IHa.
 Qed.
 
@@ -6523,9 +6523,9 @@ Lemma prop_mult_step3: forall k' a b res k,
                          length (mult_step a b res k k') = (length res)%nat.
 Proof. intro k'.
        induction k'.
-       - intros. simpl. rewrite prop_mult_step_k_h_len. simpl. omega.
+       - intros. simpl. rewrite prop_mult_step_k_h_len. simpl. lia.
        - intros. simpl.
-         rewrite IHk'. rewrite prop_mult_step_k_h_len. simpl; omega.
+         rewrite IHk'. rewrite prop_mult_step_k_h_len. simpl; lia.
 Qed.
 
 Lemma prop_and_with_bit2: forall bs1 b, length (and_with_bit bs1 b) = length bs1.
diff --git a/src/cnf/Cnf.v b/src/cnf/Cnf.v
index cc956b3..a7e3e64 100644
--- a/src/cnf/Cnf.v
+++ b/src/cnf/Cnf.v
@@ -35,10 +35,10 @@ Lemma get_or_of_imp : forall args i,
 Proof.
   unfold or_of_imp; intros args i H; case_eq (0 < PArray.length args).
   intro Heq; rewrite get_mapi.
-  replace (i == PArray.length args - 1) with false; auto; symmetry; rewrite eqb_false_spec; intro; subst i; unfold is_true in H; rewrite ltb_spec, (to_Z_sub_1 _ _ Heq) in H; omega.
-  rewrite ltb_spec; unfold is_true in H; rewrite ltb_spec, (to_Z_sub_1 _ _ Heq) in H; omega.
+  replace (i == PArray.length args - 1) with false; auto; symmetry; rewrite eqb_false_spec; intro; subst i; unfold is_true in H; rewrite ltb_spec, (to_Z_sub_1 _ _ Heq) in H; lia.
+  rewrite ltb_spec; unfold is_true in H; rewrite ltb_spec, (to_Z_sub_1 _ _ Heq) in H; lia.
   rewrite ltb_negb_geb; case_eq (PArray.length args <= 0); try discriminate; intros Heq _; assert (H1: PArray.length args = 0).
-  apply to_Z_inj; rewrite leb_spec in Heq; destruct (to_Z_bounded (PArray.length args)) as [H1 _]; change [|0|] with 0%Z in *; omega.
+  apply to_Z_inj; rewrite leb_spec in Heq; destruct (to_Z_bounded (PArray.length args)) as [H1 _]; change [|0|] with 0%Z in *; lia.
   rewrite !get_outofbound.
   rewrite default_mapi, H1; auto.
   rewrite H1; case_eq (i < 0); auto; intro H2; eelim ltb_0; eassumption.
@@ -50,7 +50,7 @@ Lemma get_or_of_imp2 : forall args i, 0 < PArray.length args ->
 Proof.
   unfold or_of_imp; intros args i Heq Hi; rewrite get_mapi; subst i.
   rewrite Int63Axioms.eqb_refl; auto.
-  rewrite ltb_spec, (to_Z_sub_1 _ _ Heq); omega.
+  rewrite ltb_spec, (to_Z_sub_1 _ _ Heq); lia.
 Qed.
 
 Lemma afold_right_impb p a :
@@ -489,7 +489,7 @@ Section CHECKER.
      exists (a.[i]);split;trivial.
      assert (H1: 0 < PArray.length a) by (apply (leb_ltb_trans _ i _); auto; apply leb_0); rewrite Int63Properties.eqb_spec in Heq'; rewrite <- (get_or_of_imp2 H1 Heq'); apply to_list_In; rewrite length_or_of_imp; auto.
      exists (Lit.neg (a.[i]));rewrite Lit.interp_neg, Heq2;split;trivial.
-     assert (H1: i < PArray.length a - 1 = true) by (rewrite ltb_spec, (to_Z_sub_1 _ _ Hlt); rewrite eqb_false_spec in Heq'; assert (H1: [|i|] <> ([|PArray.length a|] - 1)%Z) by (intro H1; apply Heq', to_Z_inj; rewrite (to_Z_sub_1 _ _ Hlt); auto); rewrite ltb_spec in Hlt; omega); rewrite <- (get_or_of_imp H1); apply to_list_In; rewrite length_or_of_imp; auto.
+     assert (H1: i < PArray.length a - 1 = true) by (rewrite ltb_spec, (to_Z_sub_1 _ _ Hlt); rewrite eqb_false_spec in Heq'; assert (H1: [|i|] <> ([|PArray.length a|] - 1)%Z) by (intro H1; apply Heq', to_Z_inj; rewrite (to_Z_sub_1 _ _ Hlt); auto); rewrite ltb_spec in Hlt; lia); rewrite <- (get_or_of_imp H1); apply to_list_In; rewrite length_or_of_imp; auto.
   Qed.
 
 End CHECKER.
diff --git a/src/lia/Lia.v b/src/lia/Lia.v
index 46bbc5d..4dd53a3 100644
--- a/src/lia/Lia.v
+++ b/src/lia/Lia.v
@@ -13,7 +13,7 @@
 Require Import Bool List Int63 PArray ZArith.
 Require Import Misc State SMT_terms Euf.
 
-Require Import RingMicromega ZMicromega Tauto Psatz.
+Require Import RingMicromega ZMicromega Coq.micromega.Tauto Psatz.
 
 Local Open Scope array_scope.
 Local Open Scope int63_scope.
@@ -507,15 +507,15 @@ Section certif.
       induction lvm;simpl;try discriminate.
       intros pvm Heq1 Heq.
       assert (1 < pvm)%positive.
-       rewrite Plt_lt;change (nat_of_P 1) with 1%nat ;omega.
+       rewrite Plt_lt;change (nat_of_P 1) with 1%nat ;lia.
       assert (Datatypes.length lvm = nat_of_P (Pos.pred pvm) - 1)%nat.
        rewrite Ppred_minus, Pminus_minus;trivial.
-       change (nat_of_P 1) with 1%nat ;try omega.
+       change (nat_of_P 1) with 1%nat ;try lia.
       revert Heq1.
       destruct (Atom.reflect_eqb h a);subst.
-      intros Heq1;inversion Heq1;clear Heq1;subst;omega.
+      intros Heq1;inversion Heq1;clear Heq1;subst;lia.
       intros Heq1;apply IHlvm in Heq1;trivial.
-      apply lt_trans with (1:= Heq1);omega.
+      apply lt_trans with (1:= Heq1);lia.
     Qed.
 
     Lemma build_pexpr_atom_aux_correct_z :
@@ -553,10 +553,10 @@ Section certif.
      induction lvm;simpl;try discriminate.
      intros pvm p Heq1 Heq.
      assert (1 < pvm)%positive.
-       rewrite Plt_lt;change (nat_of_P 1) with 1%nat ;omega.
+       rewrite Plt_lt;change (nat_of_P 1) with 1%nat ;lia.
      assert (Datatypes.length lvm = nat_of_P (Pos.pred pvm) - 1)%nat.
      rewrite Ppred_minus, Pminus_minus;trivial.
-     change (nat_of_P 1) with 1%nat ;try omega.
+     change (nat_of_P 1) with 1%nat ;try lia.
      revert Heq1.
      destruct (Atom.reflect_eqb h a);subst.
      intros Heq1;inversion Heq1;clear Heq1;subst.
@@ -564,8 +564,7 @@ Section certif.
      assert (1 < nat_of_P pvm)%nat by (rewrite Plt_lt in H;trivial).
      assert (W:=nat_of_P_pos (Pos.pred pvm)).
      assert (nat_of_P (pvm - Pos.pred pvm) - 1 = 0)%nat.
-      rewrite Pminus_minus;try omega.
-      apply Plt_lt;omega.
+      rewrite Pminus_minus;lia.
      rewrite H4;simpl.
      destruct (check_aux_interp_aux _ _ _ wf_t_atom _ _ H1) as (z,Hz).
      rewrite Hz;trivial.
@@ -575,31 +574,31 @@ Section certif.
        assert (W1:= W);rewrite <- Plt_lt in W.
        rewrite !Pminus_minus;trivial.
        assert (W2:=nat_of_P_pos (Pos.pred pvm)).
-       omega.
+       lia.
        rewrite Plt_lt.
-       apply lt_trans with (1:= W1);omega.
+       apply lt_trans with (1:= W1);lia.
      rewrite H3;simpl;apply IHlvm;trivial.
      intros _ Heq;inversion Heq;clear Heq;subst;unfold wf_vmap;
        simpl;intros (Hwf1, Hwf2);repeat split;simpl.
-     rewrite Psucc_S; assert (W:= nat_of_P_pos pvm);omega.
+     rewrite Psucc_S; assert (W:= nat_of_P_pos pvm);lia.
      rewrite Hh;trivial.
-     rewrite Psucc_S;omega.
+     rewrite Psucc_S;lia.
      intros p Hlt;
       assert (nat_of_P (Pos.succ pvm - p) - 1 = S (nat_of_P (pvm - p) - 1))%nat.
        assert (W1:= Hlt);rewrite <- Plt_lt in W1.
        rewrite !Pminus_minus;trivial.
-       rewrite Psucc_S;omega.
-       rewrite Plt_lt, Psucc_S;omega.
+       rewrite Psucc_S;lia.
+       rewrite Plt_lt, Psucc_S;lia.
      rewrite H;trivial.
      unfold is_true;rewrite <- Zlt_is_lt_bool.
-     rewrite Zpos_succ_morphism;omega.
+     rewrite Zpos_succ_morphism;lia.
      destruct (check_aux_interp_aux _ _ _ wf_t_atom _ _ Hh) as (z,Hz).
      rewrite Hz;unfold interp_vmap;simpl.
      assert (nat_of_P (Pos.succ pvm - pvm) = 1%nat).
        rewrite Pplus_one_succ_l, Pminus_minus, Pplus_plus.
-       change (nat_of_P 1) with 1%nat;omega.
+       change (nat_of_P 1) with 1%nat;lia.
        rewrite Plt_lt, Pplus_plus.
-       change (nat_of_P 1) with 1%nat;omega.
+       change (nat_of_P 1) with 1%nat;lia.
      rewrite H;simpl;rewrite Hz;trivial.
    Qed.
 
@@ -872,23 +871,23 @@ Transparent build_z_atom.
      apply foldi_down_cont_ZInd.
      intros z Hz h vm vm' pe Hh.
      assert (W:=to_Z_bounded h);rewrite to_Z_0 in Hz.
-     elimtype False;omega.
+     elimtype False;lia.
      intros i cont Hpos Hlen Hrec.
      intros h vm vm' pe;unfold is_true;rewrite <-ltb_spec;intros.
      rewrite t_interp_wf;trivial.
      apply build_pexpr_atom_aux_correct with cont h i;trivial.
      intros;apply Hrec;auto.
-     unfold is_true in H3;rewrite ltb_spec in H, H3;omega.
+     unfold is_true in H3;rewrite ltb_spec in H, H3;lia.
      unfold wf, is_true in wf_t_atom.
      rewrite forallbi_spec in wf_t_atom.
      apply wf_t_atom.
-     rewrite ltb_spec in H;rewrite leb_spec in Hlen;rewrite ltb_spec;omega.
+     rewrite ltb_spec in H;rewrite leb_spec in Hlen;rewrite ltb_spec;lia.
      unfold wt, is_true in wt_t_atom.
      rewrite forallbi_spec in wt_t_atom.
      change (is_true(Typ.eqb (get_type t_i t_func t_atom h) Typ.TZ)) in H0.
      rewrite Typ.eqb_spec in H0;rewrite <- H0.
      apply wt_t_atom.
-     rewrite ltb_spec in H;rewrite leb_spec in Hlen;rewrite ltb_spec;omega.
+     rewrite ltb_spec in H;rewrite leb_spec in Hlen;rewrite ltb_spec;lia.
    Qed.
 
    Lemma build_pexpr_correct :
@@ -925,7 +924,7 @@ Transparent build_z_atom.
      intros HH H;revert HH H1;apply build_pexpr_atom_aux_correct_z;trivial.
      rewrite <- not_true_iff_false, ltb_spec, to_Z_0 in Heq.
      assert (W:= to_Z_bounded (length t_atom)).
-     apply to_Z_inj;rewrite to_Z_0;omega.
+     apply to_Z_inj;rewrite to_Z_0;lia.
      rewrite length_t_interp;trivial.
    Qed.
 Transparent build_z_atom.
@@ -1123,14 +1122,14 @@ Transparent build_z_atom.
       (* Fatom *)
       case_eq (build_formula vm h); try discriminate; intros [vm0 f] Heq H1 H2; inversion H1; subst vm0; subst bf; apply build_formula_correct; auto.
       (* Ftrue *)
-      intros H H1; inversion H; subst vm'; subst bf; split; auto; split; [omega| ]; do 4 split; auto.
+      intros H H1; inversion H; subst vm'; subst bf; split; auto; split; [lia| ]; do 4 split; auto.
       (* Ffalse *)
-      intros H H1; inversion H; subst vm'; subst bf; split; auto; split; [omega| ]; do 3 (split; auto with smtcoq_core); discriminate.
+      intros H H1; inversion H; subst vm'; subst bf; split; auto; split; [lia| ]; do 3 (split; auto with smtcoq_core); discriminate.
       (* Fnot2 *)
       case_eq (build_var vm (Lit.blit l)); try discriminate; intros [vm0 f] Heq H H1; inversion H; subst vm0; subst bf; destruct (Hbv _ _ _ _ Heq H1) as [H2 [H3 [H4 [H5 H6]]]]; do 3 (split; auto); case_eq (Lit.is_pos l); [apply build_not2_pos_correct|apply build_not2_neg_correct]; auto.
       (* Fand *)
       simpl; unfold afold_left; case (length l == 0).
-      intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [omega| ]; do 3 (split; auto with smtcoq_core).
+      intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [lia| ]; do 3 (split; auto with smtcoq_core).
       revert vm' bf; apply (foldi_ind2 _ _ (fun f1 b => forall vm' bf, f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (forall p : positive, (Pos.to_nat p < Pos.to_nat (fst vm))%nat -> nth_error (snd vm) (Pos.to_nat (fst vm - p) - 1) = nth_error (snd vm') (Pos.to_nat (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))).
       intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto); unfold Lit.interp; rewrite Heq2; auto; simpl; split.
       intros H3 H4; rewrite <- H14 in H4; rewrite H4 in H3; discriminate.
@@ -1142,7 +1141,7 @@ Transparent build_z_atom.
       simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; case_eq (Lit.is_pos (l .[ i])); intro Heq2; simpl; rewrite <- H14; unfold Lit.interp; rewrite Heq2; split; case (Var.interp rho (Lit.blit (l .[ i]))); try rewrite andb_true_r; try rewrite andb_false_r; try (intros; split; auto with smtcoq_core); try discriminate; intros [H20 H21]; auto with smtcoq_core.
       (* For *)
       simpl; unfold afold_left; case (length l == 0).
-      intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [omega| ]; do 3 (split; auto with smtcoq_core); discriminate.
+      intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [lia| ]; do 3 (split; auto with smtcoq_core); discriminate.
       revert vm' bf; apply (foldi_ind2 _ _ (fun f1 b => forall vm' bf, f1 = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (Pos.to_nat (fst vm) <= Pos.to_nat (fst vm'))%nat /\ (forall p : positive, (Pos.to_nat p < Pos.to_nat (fst vm))%nat -> nth_error (snd vm) (Pos.to_nat (fst vm - p) - 1) = nth_error (snd vm') (Pos.to_nat (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ (b = true <-> eval_f (Zeval_formula (interp_vmap vm')) bf))).
       intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto with smtcoq_core); unfold Lit.interp; rewrite Heq2; auto with smtcoq_core; simpl; split.
       intros H3 H4; rewrite <- H14 in H4; rewrite H4 in H3; discriminate.
@@ -1154,7 +1153,7 @@ Transparent build_z_atom.
       simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; case_eq (Lit.is_pos (l .[ i])); intro Heq2; simpl; rewrite <- H14; unfold Lit.interp; rewrite Heq2; split; case (Var.interp rho (Lit.blit (l .[ i]))); try rewrite orb_false_r; try rewrite orb_true_r; auto with smtcoq_core; try (intros [H20|H20]; auto with smtcoq_core; discriminate); right; intro H20; discriminate.
       (* Fimp *)
       simpl; unfold afold_right; case (length l == 0).
-      intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [omega| ]; do 3 (split; auto with smtcoq_core).
+      intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [lia| ]; do 3 (split; auto with smtcoq_core).
       case (length l <= 1).
       case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H3 [H4 [H5 [H6 H7]]]]; do 4 (split; auto with smtcoq_core); unfold Lit.interp; rewrite Heq2; auto with smtcoq_core; simpl; split.
       intros H8 H9; rewrite <- H7 in H9; rewrite H9 in H8; discriminate.
diff --git a/src/versions/standard/Int63/Int63Properties_standard.v b/src/versions/standard/Int63/Int63Properties_standard.v
index 726bffd..137cea3 100644
--- a/src/versions/standard/Int63/Int63Properties_standard.v
+++ b/src/versions/standard/Int63/Int63Properties_standard.v
@@ -168,7 +168,7 @@ Lemma leb_ltb_eqb : forall x y, ((x <= y) = (x < y) || (x == y))%int.
 Proof.
  intros.
  apply eq_true_iff_eq.
- rewrite leb_spec, orb_true_iff, ltb_spec, eqb_spec, <- to_Z_eq;omega.
+ rewrite leb_spec, orb_true_iff, ltb_spec, eqb_spec, <- to_Z_eq;lia.
 Qed.
 
 
@@ -185,7 +185,7 @@ Proof.
  case_eq (x == y)%int;intros Heq1.
  rewrite eqb_spec in Heq1;rewrite Heq1, Z.compare_refl;trivial.
  rewrite <- not_true_iff_false, eqb_spec in Heq1.
- symmetry;change ([|x|] > [|y|]);rewrite <- to_Z_eq in Heq1;omega.
+ symmetry;change ([|x|] > [|y|]);rewrite <- to_Z_eq in Heq1;lia.
 Qed.
 
 Lemma is_zero_spec : forall x : int, is_zero x = true <-> x = 0%int.
@@ -217,7 +217,7 @@ Proof.
   destruct (Z_lt_ge_dec ([|x|] + [|y|]) wB);auto with zarith.
   assert (([|x|] + [|y|]) mod wB = [|x|] + [|y|] - wB).
   symmetry;apply Zmod_unique with 1;auto with zarith.
-  elim H;omega.
+  elim H;lia.
  rewrite Zmod_small;auto with zarith.
 Qed.
 
@@ -252,7 +252,7 @@ Proof.
   destruct (Z_lt_ge_dec ([|x|] + [|y|] + 1) wB);auto with zarith.
   assert (([|x|] + [|y|] + 1) mod wB = [|x|] + [|y|] + 1 - wB).
   symmetry;apply Zmod_unique with 1;auto with zarith.
-  elim H;omega.
+  elim H;lia.
  rewrite Zmod_small;auto with zarith.
 Qed.
 
@@ -435,12 +435,12 @@ Proof.
    split.
    - apply Z.add_nonneg_nonneg.
      + apply Z.lt_le_incl; apply Z.le_lt_trans with (2 := H). apply Z_div_pos.
-       * apply Z.lt_gt. abstract omega.
-       * abstract omega.
+       * apply Z.lt_gt. abstract lia.
+       * abstract lia.
      + apply Z_div_pos.
        * apply Z.lt_gt. assumption.
-       * abstract omega.
-   - abstract omega.
+       * abstract lia.
+   - abstract lia.
  }
  apply Hrec;rewrite lsr_spec, H0, to_Z_1;change (2^1) with 2.
  split; [ | apply sqrt_test_false;auto with zarith].
@@ -454,7 +454,7 @@ Proof.
    intro. apply Z_div_pos.
    - apply Zgt_pos_0.
    - apply Z.add_nonneg_nonneg.
-     + abstract omega.
+     + abstract lia.
      + assumption.
  }
  intros Hj1.
@@ -463,7 +463,7 @@ Proof.
  {
    apply Z_div_pos.
    - apply Zgt_pos_0.
-   - abstract omega.
+   - abstract lia.
  }
  apply sqrt_main;auto with zarith.
  split;[apply sqrt_test_true | ];auto with zarith.
@@ -478,8 +478,6 @@ Lemma iter_sqrt_correct n rec i j: 0 < [|i|] -> 0 < [|j|] ->
 Proof.
  revert rec i j; elim n; unfold iter_sqrt; fold iter_sqrt; clear n.
  intros rec i j Hi Hj Hij H31 Hrec. replace (and (Z.le (Z.pow (to_Z match ltb (div i j) j return int with | true => rec i (lsr (add31 j (div i j)) In) | false => j end) (Zpos (xO xH))) (to_Z i)) (Z.lt (to_Z i) (Z.pow (Z.add (to_Z match ltb (div i j) j return int with | true => rec i (lsr (add31 j (div i j)) In) | false => j end) (Zpos xH)) (Zpos (xO xH))))) with ([|sqrt_step rec i j|] ^ 2 <= [|i|] < ([|sqrt_step rec i j|] + 1) ^ 2) by reflexivity. apply sqrt_step_correct; auto with zarith.
- intros; apply Hrec; auto with zarith.
- rewrite Zpower_0_r; auto with zarith.
  intros n Hrec rec i j Hi Hj Hij H31 HHrec.
  replace (and (Z.le (Z.pow (to_Z match ltb (div i j) j return int with | true => iter_sqrt n (iter_sqrt n rec) i (lsr (add31 j (div i j)) In) | false => j end) (Zpos (xO xH))) (to_Z i)) (Z.lt (to_Z i) (Z.pow (Z.add (to_Z match ltb (div i j) j return int with | true => iter_sqrt n (iter_sqrt n rec) i (lsr (add31 j (div i j)) In) | false => j end) (Zpos xH)) (Zpos (xO xH))))) with ([|sqrt_step (iter_sqrt n (iter_sqrt n rec)) i j|] ^ 2 <= [|i|] < ([|sqrt_step (iter_sqrt n (iter_sqrt n rec)) i j|] + 1) ^ 2) by reflexivity.
  apply sqrt_step_correct; auto.
@@ -498,7 +496,6 @@ Proof.
  intros i; unfold sqrt.
  rewrite compare_spec. case Z.compare_spec; rewrite to_Z_1;
    intros Hi; auto with zarith.
- repeat rewrite Zpower_2; auto with zarith.
  apply iter_sqrt_correct; auto with zarith;
   rewrite lsr_spec, to_Z_1; change (2^1) with 2;  auto with zarith.
   replace ([|i|]) with (1 * 2 + ([|i|] - 2))%Z; try ring.
@@ -618,14 +615,14 @@ Proof.
       + assumption.
     - apply Z_div_pos.
       + apply Zgt_pos_0.
-      + abstract omega.
+      + abstract lia.
   }
   assert ([|i|]/2 < wB/2); auto with zarith.
   apply Zdiv_lt_upper_bound; auto with zarith.
  apply Hrec; rewrite H; clear u H.
  assert (Hf1: 0 <= [||WW ih il||]/ [|j|]) by (apply Z_div_pos; auto with zarith).
  case (Zle_lt_or_eq 1 ([|j|])); auto with zarith; intros Hf2.
- 2: contradict Heq0; apply Zle_not_lt; rewrite <- Hf2, Zdiv_1_r; assert (H10: forall (x:Z), 0 < x -> 1 <= x) by (intros; omega); auto.
+ 2: contradict Heq0; apply Zle_not_lt; rewrite <- Hf2, Zdiv_1_r; assert (H10: forall (x:Z), 0 < x -> 1 <= x) by (intros; lia); auto.
  split.
  replace ([|j|] + [||WW ih il||]/ [|j|])%Z with
         (1 * 2 + (([|j|] - 2) + [||WW ih il||] / [|j|])); try ring.
@@ -635,7 +632,7 @@ Proof.
    apply Z_div_pos.
    - apply Zgt_pos_0.
    - apply Z.add_nonneg_nonneg.
-     + abstract omega.
+     + abstract lia.
      + assumption.
  }
  apply sqrt_test_false; auto with zarith.
@@ -662,8 +659,6 @@ Lemma iter2_sqrt_correct n rec ih il j:
 Proof.
  revert rec ih il j; elim n; unfold iter2_sqrt; fold iter2_sqrt; clear n.
  intros rec ih il j Hi Hj Hij Hrec; apply sqrt2_step_correct; auto with zarith.
- intros; apply Hrec; auto with zarith.
- rewrite Zpower_0_r; auto with zarith.
  intros n Hrec rec ih il j Hi Hj Hij HHrec.
  apply sqrt2_step_correct; auto.
  intros j1 Hj1  Hjp1; apply Hrec; auto with zarith.
@@ -720,13 +715,11 @@ Lemma sqrt2_spec : forall x y,
  case (to_Z_bounded s); intros _ Hps.
  case (to_Z_bounded ih1); intros Hpih1 _; auto with zarith.
  apply Z.le_trans with (([|ih1|] + 2) * wB); auto with zarith.
- rewrite Zmult_plus_distr_l.
- assert (2 * [|s|] + 1 <= 2 * wB); auto with zarith.
  unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto.
  intros H2; split.
  unfold zn2z_to_Z; rewrite <- H2; ring.
  replace (wB + ([|il|] - [|il1|])) with ([||WW ih il||] - ([|s|] * [|s|])).
- rewrite <-Hbin in Hs2; assert (([||WW ih il||] < [|s|] * [|s|] + 2 * [|s|] + 1) -> ([||WW ih il||] - [|s|] * [|s|] <= 2 * [|s|])) by omega; auto.
+ rewrite <-Hbin in Hs2; assert (([||WW ih il||] < [|s|] * [|s|] + 2 * [|s|] + 1) -> ([||WW ih il||] - [|s|] * [|s|] <= 2 * [|s|])) by lia; auto.
  rewrite Hihl1; unfold zn2z_to_Z; rewrite <- H2; ring.
  unfold interp_carry.
  case (Zle_lt_or_eq [|ih|] [|ih1|]); auto with zarith; intros H.
@@ -743,7 +736,7 @@ Lemma sqrt2_spec : forall x y,
  unfold zn2z_to_Z; ring[Hil2 H].
  replace [|il2|] with ([||WW ih il||] - [||WW ih1 il1||]).
  unfold zn2z_to_Z at 2; rewrite <-Hihl1.
- rewrite <-Hbin in Hs2; assert (([||WW ih il||] < [|s|] * [|s|] + 2 * [|s|] + 1) -> ([||WW ih il||] - [|s|] * [|s|] <= 2 * [|s|])) by omega; auto.
+ rewrite <-Hbin in Hs2; assert (([||WW ih il||] < [|s|] * [|s|] + 2 * [|s|] + 1) -> ([||WW ih il||] - [|s|] * [|s|] <= 2 * [|s|])) by lia; auto.
  unfold zn2z_to_Z; rewrite H, Hil2; ring.
  unfold interp_carry in Hil2 |- *.
  assert (Hsih: [|ih - 1|] = [|ih|] - 1).
@@ -767,7 +760,6 @@ Lemma sqrt2_spec : forall x y,
  assert (2 * [|s|] + 1 <= 2 * wB); auto with zarith.
  apply Z.le_trans with ([|ih1|] * wB + 2 * wB); auto with zarith.
  assert (Hi: ([|ih1|] + 3) * wB <= [|ih|] * wB); auto with zarith.
- rewrite Zmult_plus_distr_l in Hi; auto with zarith.
  unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto.
  intros H2; unfold zn2z_to_Z; rewrite <-H2.
  split.
@@ -775,7 +767,7 @@ Lemma sqrt2_spec : forall x y,
  rewrite <-Hil2; ring.
  replace (1 * wB + [|il2|]) with ([||WW ih il||] - [||WW ih1 il1||]).
  unfold zn2z_to_Z at 2; rewrite <-Hihl1.
- rewrite <-Hbin in Hs2; assert (([||WW ih il||] < [|s|] * [|s|] + 2 * [|s|] + 1) -> ([||WW ih il||] - [|s|] * [|s|] <= 2 * [|s|])) by omega; auto.
+ rewrite <-Hbin in Hs2; assert (([||WW ih il||] < [|s|] * [|s|] + 2 * [|s|] + 1) -> ([||WW ih il||] - [|s|] * [|s|] <= 2 * [|s|])) by lia; auto.
  unfold zn2z_to_Z; rewrite <-H2.
  replace [|il|] with (([|il|] - [|il1|]) + [|il1|]); try ring.
  rewrite <-Hil2; ring.
@@ -803,7 +795,7 @@ Lemma sqrt2_spec : forall x y,
  rewrite <-Hil2; ring.
  replace [|il2|] with ([||WW ih il||] - [||WW ih1 il1||]).
  unfold zn2z_to_Z at 2; rewrite <- Hihl1.
- rewrite <-Hbin in Hs2; assert (([||WW ih il||] < [|s|] * [|s|] + 2 * [|s|] + 1) -> ([||WW ih il||] - [|s|] * [|s|] <= 2 * [|s|])) by omega; auto.
+ rewrite <-Hbin in Hs2; assert (([||WW ih il||] < [|s|] * [|s|] + 2 * [|s|] + 1) -> ([||WW ih il||] - [|s|] * [|s|] <= 2 * [|s|])) by lia; auto.
  unfold zn2z_to_Z.
  rewrite <-H1.
  ring_simplify.
@@ -839,9 +831,9 @@ Proof.
  unfold Zgcd_bound.
  generalize (to_Z_bounded b).
  destruct [|b|].
- unfold size; intros _; change Int31.size with 31%nat; omega.
+ unfold size; intros _; change Int31.size with 31%nat; lia.
  intros (_,H).
- cut (Psize p <= size)%nat; [ omega | rewrite <- Zpower2_Psize; auto].
+ cut (Psize p <= size)%nat; [ lia | rewrite <- Zpower2_Psize; auto].
  intros (H,_); compute in H; elim H; auto.
 Qed.
 
@@ -1506,14 +1498,14 @@ Proof.
   {
     apply Z_div_pos.
     - apply Zgt_pos_0.
-    - abstract omega.
+    - abstract lia.
   }
   apply Zdiv_lt_upper_bound; auto with zarith.
   rewrite lsr_spec, to_Z_1, Zpower_1_r; split.
   {
     apply Z_div_pos.
     - apply Zgt_pos_0.
-    - abstract omega.
+    - abstract lia.
   }
   apply Zdiv_lt_upper_bound; auto with zarith.
  assert ([|bit y 0|] <= [|bit (x lor y) 0|]); auto with zarith.
@@ -1543,14 +1535,14 @@ Proof.
    {
      apply Z_div_pos.
      - apply Zgt_pos_0.
-     - abstract omega.
+     - abstract lia.
    }
    apply Zdiv_lt_upper_bound; auto with zarith.
    rewrite lsr_spec, Zpower_1_r; split.
    {
      apply Z_div_pos.
      - apply Zgt_pos_0.
-     - abstract omega.
+     - abstract lia.
    }
    apply Zdiv_lt_upper_bound; auto with zarith.
    intros m H1 H2.
@@ -1592,14 +1584,14 @@ Proof.
  {
    apply Z_div_pos.
    - apply Zgt_pos_0.
-   - abstract omega.
+   - abstract lia.
  }
  apply Zdiv_lt_upper_bound; auto with zarith.
  rewrite lsr_spec, to_Z_1, Zpower_1_r; split.
  {
    apply Z_div_pos.
    - apply Zgt_pos_0.
-   - abstract omega.
+   - abstract lia.
  }
  apply Zdiv_lt_upper_bound; auto with zarith.
  intros _ HH m; case (to_Z_bounded m); intros H1m H2m.
@@ -1737,15 +1729,15 @@ Proof.
  assert (W1 : [|n|] <> 0) by (intros Heq;apply n0;apply to_Z_inj;trivial).
  assert (W2 := to_Z_bounded n);clear n0.
  assert (W3 : [|n-1|] = [|n|] - 1).
-   rewrite sub_spec, to_Z_1, Zmod_small;trivial;omega.
+   rewrite sub_spec, to_Z_1, Zmod_small;trivial;lia.
  assert (H1 : n = ((n-1)+1)%int).
    apply to_Z_inj;rewrite add_spec, W3.
-   rewrite Zmod_small;rewrite to_Z_1; omega.
+   rewrite Zmod_small;rewrite to_Z_1; lia.
  destruct (reflect_ltb (n-1) digits).
   rewrite <- ltb_spec in l.
   rewrite H1, <- !bit_half, H;trivial.
  assert ((digits <= n)%int = true).
-  rewrite leb_spec;omega.
+  rewrite leb_spec;lia.
  rewrite !bit_M;trivial.
 Qed.
 
@@ -1774,13 +1766,13 @@ Proof.
  intros x;rewrite ltb_spec, ltb_spec, add_spec.
  intros; assert (W:= to_Z_bounded x); assert (W1:= to_Z_bounded max_int).
  change [|0|] with 0%Z;change [|1|] with 1%Z.
- rewrite Zmod_small;omega.
+ rewrite Zmod_small;lia.
 Qed.
 
 Lemma leb_max_int : forall x, (x <= max_int)%int = true.
 Proof.
  intros x;rewrite leb_spec;assert (W:= to_Z_bounded x).
- change [|max_int|] with (wB - 1)%Z;omega.
+ change [|max_int|] with (wB - 1)%Z;lia.
 Qed.
 
 Lemma leb_0 : forall x, 0 <= x = true.
@@ -1790,7 +1782,7 @@ Qed.
 
 Lemma ltb_0 : forall x, ~ (x < 0 = true).
 Proof.
- intros x;rewrite ltb_spec, to_Z_0;destruct (to_Z_bounded x);omega.
+ intros x;rewrite ltb_spec, to_Z_0;destruct (to_Z_bounded x);lia.
 Qed.
 
 Lemma leb_trans : forall x y z, x <= y = true ->  y <= z = true -> x <= z = true.
@@ -1815,12 +1807,12 @@ Qed.
 
 Lemma gtb_not_leb : forall n m, m < n = true -> ~(n <= m = true).
 Proof.
- intros n m; rewrite ltb_spec, leb_spec;omega.
+ intros n m; rewrite ltb_spec, leb_spec;lia.
 Qed.
 
 Lemma leb_not_gtb : forall n m, m <= n = true -> ~(n < m = true).
 Proof.
- intros n m; rewrite ltb_spec, leb_spec;omega.
+ intros n m; rewrite ltb_spec, leb_spec;lia.
 Qed.
 
 Lemma leb_refl : forall n, n <= n = true.
@@ -1833,7 +1825,7 @@ Proof.
  intros x y;apply Bool.eq_true_iff_eq;split;intros.
  apply Bool.eq_true_not_negb;apply leb_not_gtb;trivial.
  rewrite Bool.negb_true_iff, <- Bool.not_true_iff_false in H.
- rewrite leb_spec; rewrite ltb_spec in H;omega.
+ rewrite leb_spec; rewrite ltb_spec in H;lia.
 Qed.
 
 Lemma ltb_negb_geb : forall x y, x < y = negb (y <= x).
@@ -1844,21 +1836,21 @@ Qed.
 Lemma to_Z_sub_gt : forall x y, y <= x = true -> [|x - y|] = ([|x|] - [|y|])%Z.
 Proof.
  intros x y;assert (W:= to_Z_bounded x);assert (W0:= to_Z_bounded y);
-   rewrite leb_spec;intros;rewrite sub_spec, Zmod_small;omega.
+   rewrite leb_spec;intros;rewrite sub_spec, Zmod_small;lia.
 Qed.
 
 Lemma not_0_ltb : forall x, x <> 0 <-> 0 < x = true.
 Proof.
  intros x;rewrite ltb_spec, to_Z_0;assert (W:=to_Z_bounded x);split.
- intros Hd;assert ([|x|] <> 0)%Z;[ | omega].
+ intros Hd;assert ([|x|] <> 0)%Z;[ | lia].
    intros Heq;elim Hd;apply to_Z_inj;trivial.
  intros Hlt Heq;elimtype False.
- assert ([|x|] = 0)%Z;[ rewrite Heq, to_Z_0;trivial | omega].
+ assert ([|x|] = 0)%Z;[ rewrite Heq, to_Z_0;trivial | lia].
 Qed.
 
 Lemma not_ltb_refl : forall i, ~(i < i = true).
 Proof.
- intros;rewrite ltb_spec;omega.
+ intros;rewrite ltb_spec;lia.
 Qed.
 
 Lemma to_Z_sub_1 : forall x y, y < x = true -> ([| x - 1|] = [|x|] - 1)%Z.
@@ -1876,7 +1868,7 @@ Qed.
 Lemma to_Z_add_1 : forall x y, x < y = true -> [|x+1|] = ([|x|] + 1)%Z.
 Proof.
   intros x y;assert (W:= to_Z_bounded x);assert (W0:= to_Z_bounded y);
-   rewrite ltb_spec;intros;rewrite add_spec, to_Z_1, Zmod_small;omega.
+   rewrite ltb_spec;intros;rewrite add_spec, to_Z_1, Zmod_small;lia.
 Qed.
 
 Lemma ltb_leb_sub1 : forall x i,  x <> 0 -> (i < x = true <-> i <= x - 1 = true).
@@ -2045,7 +2037,7 @@ Proof.
  rewrite foldi_cont_lt;[ | trivial].
  apply Hf;trivial. rewrite leb_spec;rewrite ltb_spec in Hlt;auto with zarith.
  assert ([|i|] + 1 = [|i + 1|])%Z.
-  rewrite ltb_spec in Hlt;assert (W:= to_Z_bounded i);rewrite add_spec, to_Z_1, Zmod_small;omega.
+  rewrite ltb_spec in Hlt;assert (W:= to_Z_bounded i);rewrite add_spec, to_Z_1, Zmod_small;lia.
  rewrite H;apply Hr;trivial.
  assert (max < min = true) by (rewrite ltb_negb_geb,Heq;trivial).
  rewrite foldi_cont_gt;trivial;apply Ha;rewrite <- ltb_spec;trivial.
@@ -2073,15 +2065,15 @@ Qed.
 (*   repeat change (2^1)%Z with 2%Z. *)
 (*   rewrite Zmult_mod_distr_l;trivial. *)
 (* Transparent Z_of_nat. *)
-(*   rewrite inj_S;omega. *)
+(*   rewrite inj_S;lia. *)
 (*   discriminate. *)
 (*   split;[discriminate | trivial]. *)
 (*   compute;trivial. *)
 (*   assert (W:0 <= Zpos p mod 2 ^ Z_of_nat k < 2 ^ Z_of_nat k). *)
 (*    apply Z.mod_pos_bound;auto with zarith. *)
-(*   change (2^1)%Z with 2%Z;split;try omega. *)
+(*   change (2^1)%Z with 2%Z;split;try lia. *)
 (*   apply Z.lt_le_trans with (2 ^ Z_of_nat (S k)). *)
-(*   rewrite inj_S, Zpower_Zsucc;omega. *)
+(*   rewrite inj_S, Zpower_Zsucc;lia. *)
 (*   unfold wB;apply Zpower_le_monotone;auto with zarith. *)
 (*   split;auto using inj_le with zarith. *)
 (*   auto with zarith. *)
@@ -2096,9 +2088,9 @@ Qed.
 (*   rewrite Zmult_mod_distr_l;trivial. *)
 (*   assert (W:0 <= Zpos p mod 2 ^ Z_of_nat k < 2 ^ Z_of_nat k). *)
 (*    apply Z.mod_pos_bound;auto with zarith. *)
-(*   change (2^1)%Z with 2%Z;split;try omega. *)
+(*   change (2^1)%Z with 2%Z;split;try lia. *)
 (*   apply Z.lt_le_trans with (2 ^ Z_of_nat (S k)). *)
-(*   rewrite inj_S, Zpower_Zsucc;omega. *)
+(*   rewrite inj_S, Zpower_Zsucc;lia. *)
 (*   unfold wB;apply Zpower_le_monotone;auto with zarith. *)
 (*   split;auto using inj_le with zarith. *)
 (*   auto with zarith. *)
@@ -2172,10 +2164,10 @@ Proof.
  apply foldi_cont_ZInd;intros;red.
  rewrite Zlt_is_lt_bool in H1;rewrite H1;trivial.
  case_eq (Zlt_bool [|max|] [|i|]);intros.
-  rewrite <- Zlt_is_lt_bool in H4;rewrite leb_spec in H2;elimtype False;omega.
+  rewrite <- Zlt_is_lt_bool in H4;rewrite leb_spec in H2;elimtype False;lia.
  clear H4; revert H3;unfold P'.
  case_eq (Zlt_bool [|max|] ([|i|] + 1));intros;auto.
-  rewrite <- Zlt_is_lt_bool in H3; assert ([|i|] = [|max|]) by (rewrite leb_spec in H2;omega).
+  rewrite <- Zlt_is_lt_bool in H3; assert ([|i|] = [|max|]) by (rewrite leb_spec in H2;lia).
   rewrite H4, <- H6;apply H0;trivial.
  revert H1;unfold P'.
  case_eq (Zlt_bool [|max|] [|min|]);auto.
@@ -2234,7 +2226,7 @@ Proof.
  clear Ha;revert cont H Heq.
  pattern max at 1 2 4 5;apply int_ind;trivial.
  intros; assert (0 = min).
-   apply to_Z_inj;revert Heq;rewrite leb_spec, to_Z_0;omega.
+   apply to_Z_inj;revert Heq;rewrite leb_spec, to_Z_0;lia.
  rewrite foldi_down_cont_eq;subst;auto.
  intros i Hmaxi Hr cont Hcont Hmin Hmax.
  generalize Hmin;rewrite leb_ltb_eqb;case_eq (min < i+1);simpl;intros Hlt Hmin'.
@@ -2245,12 +2237,12 @@ Proof.
     assert (W2 := to_Z_bounded max_int);rewrite add_spec, to_Z_1, Zmod_small;auto with zarith.
  assert (i + 1 - 1 = i).
   rewrite leb_spec in *;rewrite ltb_spec in *.
-  assert (W1:= to_Z_bounded i); apply to_Z_inj;rewrite sub_spec,to_Z_1, Zmod_small;try omega.
+  assert (W1:= to_Z_bounded i); apply to_Z_inj;rewrite sub_spec,to_Z_1, Zmod_small;try lia.
  assert ([|i|] = [|i+1|]-1)%Z.
    rewrite <- H;ring.
  rewrite <- H1, H0;apply Hr;trivial.
- rewrite ltb_spec in Hlt;rewrite leb_spec;omega.
- rewrite leb_spec in Hmax |- *;omega.
+ rewrite ltb_spec in Hlt;rewrite leb_spec;lia.
+ rewrite leb_spec in Hmax |- *;lia.
  rewrite eqb_spec in Hmin';subst;rewrite foldi_down_cont_eq;auto.
  assert (max < min = true) by (rewrite ltb_negb_geb,Heq;trivial).
  rewrite foldi_down_cont_lt;trivial.
@@ -2283,10 +2275,10 @@ Proof.
  apply foldi_down_cont_ZInd;intros;red.
  rewrite Zlt_is_lt_bool in H1;rewrite H1;trivial.
  case_eq (Zlt_bool [|i|] [|min|]);intros.
-  rewrite <- Zlt_is_lt_bool in H4;rewrite leb_spec in H1;elimtype False;omega.
+  rewrite <- Zlt_is_lt_bool in H4;rewrite leb_spec in H1;elimtype False;lia.
  clear H4;revert H3;unfold P'.
  case_eq (Zlt_bool ([|i|] - 1) [|min|]);intros;auto.
-  rewrite <- Zlt_is_lt_bool in H3; assert ([|i|] = [|min|]) by (rewrite leb_spec in H1;omega).
+  rewrite <- Zlt_is_lt_bool in H3; assert ([|i|] = [|min|]) by (rewrite leb_spec in H1;lia).
   rewrite H4, <- H6. apply H0;trivial.
  revert H1;unfold P'.
  case_eq (Zlt_bool [|max|] [|min|]);auto.
@@ -2356,8 +2348,8 @@ Proof.
       replace (min + i + 1) with (min + 1 + i).
       rewrite leb_spec, (add_spec (min+1)).
       unfold is_true in Hi1;rewrite leb_spec in *; rewrite ltb_spec in *.
-      rewrite sub_spec in Hi1;rewrite Zmod_small in Hi1;[ | omega].
-      rewrite Zmod_small;omega.
+      rewrite sub_spec in Hi1;rewrite Zmod_small in Hi1;[ | lia].
+      rewrite Zmod_small;lia.
       rewrite <- !add_assoc, (add_comm 1 i);trivial.
     rewrite leb_ltb_eqb in H2;revert H2.
     case_eq (min + 1 < min + i + 1).
@@ -2365,12 +2357,12 @@ Proof.
       rewrite foldi_down_gt with (from := min + i + 1);trivial.
       replace (min + i + 1 - 1) with (min + i).
       apply Hrec.
-      apply leb_trans with (i+1);[rewrite leb_spec;omega | trivial].
+      apply leb_trans with (i+1);[rewrite leb_spec;lia | trivial].
       apply to_Z_inj;rewrite sub_spec, (add_spec (min + i)), to_Z_1, Zminus_mod_idemp_l.
       assert (H100: forall (x:Z), (x + 1 - 1)%Z = x) by (intros; ring). rewrite H100.
       rewrite Zmod_small;auto using to_Z_bounded.
       apply leb_ltb_trans with (2:= Hlt).
-      rewrite leb_spec;omega.
+      rewrite leb_spec;lia.
     simpl;rewrite eqb_spec;intros _ Heq.
     rewrite <- Heq.
     rewrite foldi_down_gt.
@@ -2379,7 +2371,7 @@ Proof.
      apply to_Z_inj;rewrite sub_spec, add_spec, to_Z_1, Zminus_mod_idemp_l.
      replace ([|min|] + 1 - 1)%Z with [|min|] by ring.
      rewrite Zmod_small;auto using to_Z_bounded.
-     rewrite ltb_spec;omega.
+     rewrite ltb_spec;lia.
   generalize (H2 (leb_refl _) a).
   replace (min + (max - min)) with max;trivial.
   apply to_Z_inj;rewrite add_spec, sub_spec, Zplus_mod_idemp_r.
@@ -2424,7 +2416,7 @@ Proof.
   rewrite of_to_Z;generalize H2;rewrite leb_ltb_eqb, orb_true_iff;intros [Hlt | Heq].
   rewrite foldi_cont_lt;[apply H0 | ];trivial.
   revert H3;case_eq (Zlt_bool [|max|] ([|i|] + 1)).
-  rewrite <- Zlt_is_lt_bool;rewrite ltb_spec in Hlt;intros;elimtype False;omega.
+  rewrite <- Zlt_is_lt_bool;rewrite ltb_spec in Hlt;intros;elimtype False;lia.
   rewrite <- (to_Z_add_1 _ _ Hlt), of_to_Z; intros _ W;exact W.
   rewrite eqb_spec in Heq;subst.
   rewrite foldi_cont_eq;[apply H0 | ];trivial.
@@ -2467,10 +2459,10 @@ Proof.
   apply foldi_cont_ZInd2;intros;red.
   rewrite Zlt_is_lt_bool in H1;rewrite H1;auto.
   case_eq (Zlt_bool [|max|] [|i|]);intros.
-  rewrite <- Zlt_is_lt_bool in H4;rewrite leb_spec in H2;elimtype False;omega.
+  rewrite <- Zlt_is_lt_bool in H4;rewrite leb_spec in H2;elimtype False;lia.
   clear H4; revert H3;unfold P'.
   case_eq (Zlt_bool [|max|] ([|i|] + 1));intros;auto.
-  rewrite <- Zlt_is_lt_bool in H3; assert ([|i|] = [|max|]) by (rewrite leb_spec in H2;omega).
+  rewrite <- Zlt_is_lt_bool in H3; assert ([|i|] = [|max|]) by (rewrite leb_spec in H2;lia).
   destruct H4;subst;rewrite <- H6;apply H0;trivial.
   revert H1;unfold P'.
   case_eq (Zlt_bool [|max|] [|min|]);auto.
@@ -2548,7 +2540,7 @@ Proof.
   rewrite of_to_Z;generalize H1;rewrite leb_ltb_eqb, orb_true_iff;intros [Hlt | Heq].
   rewrite foldi_down_cont_gt;[apply H0 | ];trivial.
   revert H3;case_eq (Zlt_bool ([|i|] - 1) [|min|]).
-  rewrite <- Zlt_is_lt_bool;rewrite ltb_spec in Hlt;intros;elimtype False;omega.
+  rewrite <- Zlt_is_lt_bool;rewrite ltb_spec in Hlt;intros;elimtype False;lia.
   rewrite <- (to_Z_sub_1 _ _ Hlt), of_to_Z; intros _ W;exact W.
   rewrite eqb_spec in Heq;subst.
   rewrite foldi_down_cont_eq;[apply H0 | ];trivial.
@@ -2593,10 +2585,10 @@ Proof.
   apply foldi_down_cont_ZInd2;intros;red.
   rewrite Zlt_is_lt_bool in H2;rewrite H2;auto.
   case_eq (Zlt_bool [|i|] [|min|]);intros.
-  rewrite <- Zlt_is_lt_bool in H5;rewrite leb_spec in H2;elimtype False;omega.
+  rewrite <- Zlt_is_lt_bool in H5;rewrite leb_spec in H2;elimtype False;lia.
   clear H5;revert H4;unfold P'.
   case_eq (Zlt_bool ([|i|] - 1) [|min|]);intros;auto.
-  rewrite <- Zlt_is_lt_bool in H4; assert ([|i|] = [|min|]) by (rewrite leb_spec in H2;omega).
+  rewrite <- Zlt_is_lt_bool in H4; assert ([|i|] = [|min|]) by (rewrite leb_spec in H2;lia).
   destruct H5;subst;rewrite <- H7;apply H1;trivial.
   revert H2;unfold P'.
   case_eq (Zlt_bool [|max|] [|min|]);auto.
@@ -2640,11 +2632,11 @@ Proof.
  unfold forallb;intros f from to.
  setoid_rewrite leb_spec.
  apply foldi_cont_ZInd.
- intros;split;[intros;elimtype False;omega | trivial].
+ intros;split;[intros;elimtype False;lia | trivial].
  intros i cont Hfr Hto Hcont.
  case_eq (f i);intros Heq.
  rewrite Hcont;clear Hcont;split;auto with zarith;intros.
- assert (H2 : ([|i0|] = [|i|] \/ [|i|] + 1 <= [|i0|])%Z) by omega; destruct H2;auto with zarith.
+ assert (H2 : ([|i0|] = [|i|] \/ [|i|] + 1 <= [|i0|])%Z) by lia; destruct H2;auto with zarith.
  apply to_Z_inj in H2;rewrite H2;trivial.
  split;[discriminate | intros].
  rewrite leb_spec in Hto;rewrite <- Heq;auto with zarith.
@@ -2667,7 +2659,7 @@ Proof.
  unfold existsb;intros.
  repeat setoid_rewrite andb_true_iff;setoid_rewrite leb_spec.
  apply foldi_cont_ZInd.
- intros;split;[discriminate | intros [i [W1 W2]];elimtype False;omega].
+ intros;split;[discriminate | intros [i [W1 W2]];elimtype False;lia].
  intros i cont Hfr Hto Hcont.
  case_eq (f i);intros Heq.
   split;trivial.
@@ -2696,7 +2688,7 @@ Proof.
  apply leb_0.
  rewrite ltb_spec in H.
  destruct (to_Z_bounded i);rewrite leb_spec.
- change [|digits - 1 |] with ([|digits|] - 1)%Z;omega.
+ change [|digits - 1 |] with ([|digits|] - 1)%Z;lia.
 Qed.
 
 Lemma land_max_int_l : forall i, max_int land i = i.
@@ -2707,7 +2699,7 @@ Proof.
   rewrite <- leb_spec in l.
   rewrite !bit_M;trivial.
   rewrite bit_max_int;trivial.
-  rewrite ltb_spec;omega.
+  rewrite ltb_spec;lia.
 Qed.
 
 Lemma land_max_int_r : forall i, i land max_int = i.