diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
index 7a72eee..c54534c 100644
--- a/.github/workflows/coq-action.yml
+++ b/.github/workflows/coq-action.yml
@@ -12,12 +12,10 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '8.12'
-          - '8.13'
-          - '8.14'
-          - '8.15'
           - '8.16'
           - '8.17'
+          - '8.18'
+          - '8.19'
           - 'dev'
         ocaml_version:
           - 'default'
diff --git a/.gitignore b/.gitignore
index 6ddf536..318f794 100644
--- a/.gitignore
+++ b/.gitignore
@@ -49,8 +49,10 @@ time-of-build-pretty.log
 .CoqMakefile.d
 CoqMakefile*
 Makefile.coq*
+Makefile.conf
 
 _build
 
 docs
 /.vscode
+.DS_Store
\ No newline at end of file
diff --git a/CITATION.cff b/CITATION.cff
index 86a29bd..8cc2aa4 100644
--- a/CITATION.cff
+++ b/CITATION.cff
@@ -4,7 +4,7 @@ title: "INQWIRE QuantumLib"
 abstract: "QuantumLib is a Coq library for reasoning about quantum programs."
 authors:
   - name: "The INQWIRE Developers"
-version: 1.0.0
+version: 1.3.0
 date-released: 2022-01-06
 license: MIT
 repository-code: "https://github.com/inQWIRE/QuantumLib"
diff --git a/DiscreteProb.v b/DiscreteProb.v
index 30d905d..5d20d2c 100644
--- a/DiscreteProb.v
+++ b/DiscreteProb.v
@@ -102,7 +102,7 @@ Lemma sample_ub_lt :  forall l r,
 Proof.
   induction l; intros. unfold sum_over_list in H. simpl in H. lra.
   simpl. destruct (Rlt_le_dec r a). lia.
-  apply lt_n_S. apply IHl. rewrite sum_over_list_cons in H. lra.
+  apply -> Nat.succ_lt_mono. apply IHl. rewrite sum_over_list_cons in H. lra.
 Qed.
 
 Lemma sample_lb : forall l r, (0 <= sample l r)%nat.
@@ -1498,12 +1498,12 @@ Proof.
     replace (2 ^ (n + k))%nat with (2 ^ n * 2 ^ k)%nat by unify_pows_two.
     apply (Nat.mul_le_mono_r _ _ (2^k)%nat) in H0.
     rewrite Nat.mul_sub_distr_r in H0.
-    rewrite mult_1_l in H0.
+    rewrite Nat.mul_1_l in H0.
     apply (Nat.add_lt_le_mono x0 (2^k)%nat) in H0; auto.
-    rewrite <- le_plus_minus in H0.
-    rewrite plus_comm in H0.
+    rewrite <- le_plus_minus' in H0.
+    rewrite Nat.add_comm in H0.
     assumption.
-    destruct (mult_O_le (2^k) (2^n))%nat; auto.
+    destruct (Arith_prebase.mult_O_le_stt (2^k) (2^n))%nat; auto.
     assert (2 <> 0)%nat by lia.
     apply (pow_positive 2 n) in H2.
     lia.
diff --git a/Eigenvectors.v b/Eigenvectors.v
index 33760ab..8d8e0a4 100644
--- a/Eigenvectors.v
+++ b/Eigenvectors.v
@@ -259,7 +259,7 @@ Proof. induction n as [| n'].
              rewrite p in H1; easy. }
            rewrite H', Pplus_comm, Pplus_degree2; auto. 
            rewrite H1. 
-           apply le_lt_n_Sm.
+           apply Nat.lt_succ_r.
            apply Psum_degree; intros. 
            assert (H2 : prep_mat A (S i) 0 = [A (S i) 0]).
            { unfold prep_mat. 
@@ -356,7 +356,7 @@ Proof. intros.
        prep_matrix_equality.
        unfold get_vec, form_basis.
        bdestruct (y =? 0).
-       rewrite <- beq_nat_refl, H0; easy.
+       rewrite Nat.eqb_refl, H0; easy.
        unfold WF_Matrix in H.
        rewrite H; try easy.
        right. 
@@ -885,7 +885,7 @@ Proof. induction m2 as [| m2'].
          exists Zero.
          split. easy.
          rewrite smash_zero; try easy.
-         rewrite plus_0_r.
+         rewrite Nat.add_0_r.
          apply H2.
        - intros. 
          rewrite (split_col T2) in *.
@@ -1180,8 +1180,8 @@ Proof. intros a b m H0 Hdiv Hmod.
        rewrite Hdiv in Hmod.
        assert (H : m * (b / m) + (a - m * (b / m)) = m * (b / m) + (b - m * (b / m))).
        { rewrite Hmod. reflexivity. }
-       rewrite <- (le_plus_minus  (m * (b / m)) a) in H.
-       rewrite <- (le_plus_minus  (m * (b / m)) b) in H.
+       rewrite <- (le_plus_minus'  (m * (b / m)) a) in H.
+       rewrite <- (le_plus_minus'  (m * (b / m)) b) in H.
        apply H.
        apply Nat.mul_div_le; apply H0.
        rewrite <- Hdiv; apply Nat.mul_div_le; apply H0.
diff --git a/GenMatrix.v b/GenMatrix.v
index 67391e4..0b2d196 100644
--- a/GenMatrix.v
+++ b/GenMatrix.v
@@ -316,8 +316,8 @@ Ltac by_cell :=
   let Hi := fresh "Hi" in 
   let Hj := fresh "Hj" in 
   intros i j Hi Hj; try solve_end;
-  repeat (destruct i as [|i]; simpl; [|apply Nat.succ_lt_mono in Hi]; try solve_end); clear Hi;
-  repeat (destruct j as [|j]; simpl; [|apply Nat.succ_lt_mono in Hj]; try solve_end); clear Hj.
+  repeat (destruct i as [|i]; simpl; [|apply <- Nat.succ_lt_mono in Hi]; try solve_end); clear Hi;
+  repeat (destruct j as [|j]; simpl; [|apply <- Nat.succ_lt_mono in Hj]; try solve_end); clear Hj.
 
 Ltac lgma' :=
   apply genmat_equiv_eq;
@@ -3639,7 +3639,7 @@ Proof. intros.
        simpl.  
        autorewrite with R_db.
        rewrite Rmult_comm.
-       rewrite Rinv_mult_distr; try easy. 
+       rewrite Rinv_mult; try easy. 
        rewrite <- Rmult_comm.
        rewrite <- Rmult_assoc.
        rewrite Rinv_r; try easy.
@@ -3648,7 +3648,7 @@ Proof. intros.
        unfold Cinv.
        simpl. 
        autorewrite with R_db.
-       rewrite Rinv_mult_distr; try easy. 
+       rewrite Rinv_mult; try easy. 
        rewrite <- Rmult_assoc.
        rewrite Rinv_r; try easy.
        autorewrite with R_db.
diff --git a/Matrix.v b/Matrix.v
index f1aa2e9..7fef483 100644
--- a/Matrix.v
+++ b/Matrix.v
@@ -306,8 +306,8 @@ Ltac by_cell :=
   let Hi := fresh "Hi" in 
   let Hj := fresh "Hj" in 
   intros i j Hi Hj; try solve_end;
-  repeat (destruct i as [|i]; simpl; [|apply lt_S_n in Hi]; try solve_end); clear Hi;
-  repeat (destruct j as [|j]; simpl; [|apply lt_S_n in Hj]; try solve_end); clear Hj.
+  repeat (destruct i as [|i]; simpl; [|apply <- Nat.succ_lt_mono in Hi]; try solve_end); clear Hi;
+  repeat (destruct j as [|j]; simpl; [|apply <- Nat.succ_lt_mono in Hj]; try solve_end); clear Hj.
 
 Ltac lma' :=
   apply mat_equiv_eq;
@@ -543,7 +543,7 @@ Ltac show_wf :=
   let y := fresh "y" in
   let H := fresh "H" in
   intros x y [H | H];
-  apply le_plus_minus in H; rewrite H;
+  apply le_plus_minus' in H; rewrite H;
   cbv;
   destruct_m_eq;
   try lca.
@@ -1188,10 +1188,10 @@ Proof.
   unfold I, kron.
   prep_matrix_equality.
   bdestruct (x =? y); rename H into Eq; subst.
-  + repeat rewrite <- beq_nat_refl; simpl.
+  + repeat rewrite Nat.eqb_refl; simpl.
     destruct n.
     - simpl.
-      rewrite mult_0_r.
+      rewrite Nat.mul_0_r.
       bdestruct (y <? 0); try lia.
       autorewrite with C_db; reflexivity.
     - bdestruct (y mod S n <? S n). 
@@ -1209,13 +1209,13 @@ Proof.
         simpl. apply Nat.neq_succ_0. (* `lia` will solve in 8.11+ *)
         apply Nat.div_small in L1.
         rewrite Nat.div_div in L1; try lia.
-        rewrite mult_comm.
+        rewrite Nat.mul_comm.
         assumption.
       * apply Nat.ltb_nlt in L1. 
         apply Nat.ltb_lt in L2. 
         contradict L1. 
         apply Nat.div_lt_upper_bound. lia.
-        rewrite mult_comm.
+        rewrite Nat.mul_comm.
         assumption.
   + simpl.
     bdestruct (x / n =? y / n); simpl; try lca.
@@ -1253,7 +1253,7 @@ Lemma sub_mul_mod :
     (x - y * z) mod z = x mod z.
 Proof.
   intros. bdestruct (z =? 0). subst. simpl. lia.
-  specialize (le_plus_minus_r (y * z) x H) as G.
+  specialize (le_plus_minus_r' (y * z) x H) as G.
   remember (x - (y * z)) as r.
   rewrite <- G. rewrite <- Nat.add_mod_idemp_l by easy. rewrite Nat.mod_mul by easy.
   easy.
@@ -1277,8 +1277,8 @@ Proof.
   intros. intros i j Hi Hj.
   remember (A ⊗ B ⊗ C) as LHS.
   unfold kron.  
-  rewrite (mult_comm p r) at 1 2.
-  rewrite (mult_comm q s) at 1 2.
+  rewrite (Nat.mul_comm p r) at 1 2.
+  rewrite (Nat.mul_comm q s) at 1 2.
   assert (m * p * r <> 0) by lia.
   assert (n * q * s <> 0) by lia.
   apply Nat.neq_mul_0 in H as [Hmp Hr].
@@ -1312,7 +1312,7 @@ Proof.
   prep_matrix_equality.
   destruct q.
   + simpl.
-    rewrite mult_0_r.
+    rewrite Nat.mul_0_r.
     simpl.
     rewrite Cmult_0_r.
     reflexivity. 
@@ -2622,7 +2622,7 @@ Proof. intros.
        apply big_sum_eq_bounded; intros.
        bdestruct (e + S x0 =? e); try lia; easy.
        unfold get_vec. simpl. 
-       rewrite plus_0_r; easy.
+       rewrite Nat.add_0_r; easy.
 Qed.
 
 (* shows that we can eliminate a column in a matrix using col_add_many *)
@@ -2638,12 +2638,12 @@ Proof. intros.
                      (@Mmult n m 1 (reduce_col T col) (reduce_row as' col)) i 0)%C).
        { unfold Mmult.
          replace (S m) with (col + (S (m - col))) by lia; rewrite big_sum_sum. 
-         rewrite (le_plus_minus col m); try lia; rewrite big_sum_sum. 
+         rewrite (le_plus_minus' col m); try lia; rewrite big_sum_sum. 
          apply Cplus_simplify. 
          apply big_sum_eq_bounded; intros. 
          unfold get_vec, scale, reduce_col, reduce_row. 
          bdestruct (x <? col); simpl; try lia; lca.
-         rewrite <- le_plus_minus, <- big_sum_extend_l, plus_0_r, H0; try lia. 
+         rewrite <- le_plus_minus', <- big_sum_extend_l, Nat.add_0_r, H0; try lia. 
          unfold scale; rewrite Cmult_0_l, Cplus_0_l.
          apply big_sum_eq_bounded; intros. 
          unfold get_vec, scale, reduce_col, reduce_row. 
@@ -2846,7 +2846,7 @@ Proof. intros.
        prep_matrix_equality. 
        unfold Mmult. 
        bdestruct (x <? m); try lia.
-       rewrite (le_plus_minus x m); try lia.
+       rewrite (le_plus_minus' x m); try lia.
        do 2 rewrite big_sum_sum. 
        apply Cplus_simplify. 
        apply big_sum_eq_bounded.
@@ -2858,7 +2858,7 @@ Proof. intros.
        rewrite Cplus_comm.
        rewrite (Cplus_comm (col_swap A x y x0 (x + 0)%nat * row_swap B x y (x + 0)%nat y0)%C _).
        bdestruct ((y - x - 1) <? x'); try lia.  
-       rewrite (le_plus_minus (y - x - 1) x'); try lia. 
+       rewrite (le_plus_minus' (y - x - 1) x'); try lia. 
        do 2 rewrite big_sum_sum.
        do 2 rewrite <- Cplus_assoc.
        apply Cplus_simplify. 
@@ -2915,7 +2915,7 @@ Proof. intros.
        prep_matrix_equality. 
        unfold Mmult.   
        bdestruct (x <? m); try lia.
-       rewrite (le_plus_minus x m); try lia.       
+       rewrite (le_plus_minus' x m); try lia.       
        do 2 rewrite big_sum_sum.
        apply Cplus_simplify. 
        apply big_sum_eq_bounded.
@@ -2927,7 +2927,7 @@ Proof. intros.
        rewrite Cplus_comm. 
        rewrite (Cplus_comm (col_add A x y a x0 (x + 0)%nat * B (x + 0)%nat y0)%C _).
        bdestruct ((y - x - 1) <? x'); try lia.  
-       rewrite (le_plus_minus (y - x - 1) x'); try lia. 
+       rewrite (le_plus_minus' (y - x - 1) x'); try lia. 
        do 2 rewrite big_sum_sum.
        do 2 rewrite <- Cplus_assoc.
        apply Cplus_simplify. 
@@ -3242,7 +3242,7 @@ Proof. intros.
        prep_matrix_equality. 
        bdestruct (y =? m); bdestruct (y <? m); try lia; try easy.
        rewrite H1.
-       rewrite <- minus_diag_reverse; easy. 
+       rewrite Nat.sub_diag; easy. 
        rewrite H0, H; try lia; try easy.
 Qed.
 
@@ -3533,7 +3533,7 @@ Proof. intros.
        simpl.  
        autorewrite with R_db.
        rewrite Rmult_comm.
-       rewrite Rinv_mult_distr; try easy. 
+       rewrite Rinv_mult; try easy. 
        rewrite <- Rmult_comm.
        rewrite <- Rmult_assoc.
        rewrite Rinv_r; try easy.
@@ -3542,7 +3542,7 @@ Proof. intros.
        unfold Cinv.
        simpl. 
        autorewrite with R_db.
-       rewrite Rinv_mult_distr; try easy. 
+       rewrite Rinv_mult; try easy. 
        rewrite <- Rmult_assoc.
        rewrite Rinv_r; try easy.
        autorewrite with R_db.
diff --git a/Measurement.v b/Measurement.v
index 7b5b1ec..b92d81a 100644
--- a/Measurement.v
+++ b/Measurement.v
@@ -59,7 +59,7 @@ Proof.
   unfold prob_partial_meas.
   rewrite norm_squared.
   unfold inner_product, Mmult, adjoint.
-  rewrite (@big_sum_func_distr C R _ C_is_group _ R_is_group), mult_1_l.
+  rewrite (@big_sum_func_distr C R _ C_is_group _ R_is_group), Nat.mul_1_l.
   apply big_sum_eq_bounded; intros. 
   unfold probability_of_outcome.
   assert (H' : forall c, ((Cmod c)^2)%R = fst (c^* * c)).
diff --git a/Pad.v b/Pad.v
index 442a79e..cf26225 100644
--- a/Pad.v
+++ b/Pad.v
@@ -219,29 +219,29 @@ Ltac rem_max_min :=
    unfold gt, ge, abs_diff in *;
   repeat match goal with 
   | [ H: (?a < ?b)%nat |- context[Nat.max (?a - ?b) (?b - ?a)] ] => 
-    rewrite (Max.max_r (a - b) (b - a)) by lia 
+    rewrite (Nat.max_r (a - b) (b - a)) by lia 
   | [ H: (?a < ?b)%nat |- context[Nat.max (?b - ?a) (?a - ?b)] ] => 
-    rewrite (Max.max_l (b - a) (a - b)) by lia 
+    rewrite (Nat.max_l (b - a) (a - b)) by lia 
   | [ H: (?a <= ?b)%nat |- context[Nat.max (?a - ?b) (?b - ?a)] ] => 
-    rewrite (Max.max_r (a - b) (b - a)) by lia 
+    rewrite (Nat.max_r (a - b) (b - a)) by lia 
   | [ H: (?a <= ?b)%nat |- context[Nat.max (?b - ?a) (?a - ?b)] ] => 
-    rewrite (Max.max_l (b - a) (a - b)) by lia   
+    rewrite (Nat.max_l (b - a) (a - b)) by lia   
   | [ H: (?a < ?b)%nat |- context[Nat.min ?a ?b] ] => 
-    rewrite Min.min_l by lia 
+    rewrite Nat.min_l by lia 
   | [ H: (?a < ?b)%nat |- context[Nat.max ?a ?b] ] => 
-    rewrite Max.max_r by lia 
+    rewrite Nat.max_r by lia 
   | [ H: (?a < ?b)%nat |- context[Nat.min ?b ?a] ] => 
-    rewrite Min.min_r by lia 
+    rewrite Nat.min_r by lia 
   | [ H: (?a < ?b)%nat |- context[Nat.max ?b ?a] ] => 
-    rewrite Max.max_l by lia 
+    rewrite Nat.max_l by lia 
   | [ H: (?a <= ?b)%nat |- context[Nat.min ?a ?b] ] => 
-    rewrite Min.min_l by lia 
+    rewrite Nat.min_l by lia 
   | [ H: (?a <= ?b)%nat |- context[Nat.max ?a ?b] ] => 
-    rewrite Max.max_r by lia 
+    rewrite Nat.max_r by lia 
   | [ H: (?a <= ?b)%nat |- context[Nat.min ?b ?a] ] => 
-    rewrite Min.min_r by lia 
+    rewrite Nat.min_r by lia 
   | [ H: (?a <= ?b)%nat |- context[Nat.max ?b ?a] ] => 
-    rewrite Max.max_l by lia 
+    rewrite Nat.max_l by lia 
   end.
 
 Definition pad2x2_u (dim n : nat) (u : Square 2) : Square (2^dim) := @embed dim [(u,n)].
@@ -336,7 +336,7 @@ Proof.
   intros. unfold pad2x2_u, pad2x2_ctrl, abs_diff. bdestruct_all; simpl; rem_max_min;
   Msimpl; trivial.
   + repeat rewrite Mmult_plus_distr_l; repeat rewrite Mmult_plus_distr_r.
-  rewrite le_plus_minus_r by (apply Nat.lt_le_incl; trivial).
+  rewrite le_plus_minus_r' by (apply Nat.lt_le_incl; trivial).
   repeat rewrite embed_mult; simpl.
   rewrite (embed_commutes dim [(A, m); (∣1⟩⟨1∣, n); (B, o)] [(∣1⟩⟨1∣, n); (B, o); (A, m)]).
   rewrite (embed_commutes dim [(A, m); (∣0⟩⟨0∣, n); (I 2, o)] [(∣0⟩⟨0∣, n); (I 2, o); (A, m)]).
@@ -345,7 +345,7 @@ Proof.
   all : rewrite perm_swap; apply perm_skip; apply perm_swap.
 
   + repeat rewrite Mmult_plus_distr_l; repeat rewrite Mmult_plus_distr_r.
-  rewrite le_plus_minus_r by trivial; repeat rewrite embed_mult; simpl.
+  rewrite le_plus_minus_r' by trivial; repeat rewrite embed_mult; simpl.
   rewrite (embed_commutes dim [(A, m); (B, o); (∣1⟩⟨1∣, n)] [(B, o); (∣1⟩⟨1∣, n); (A, m)]).
   rewrite (embed_commutes dim [(A, m); (I 2, o); (∣0⟩⟨0∣, n)] [(I 2, o); (∣0⟩⟨0∣, n); (A, m)]).
   trivial.
diff --git a/Permutations.v b/Permutations.v
index c122bfc..3257566 100644
--- a/Permutations.v
+++ b/Permutations.v
@@ -162,7 +162,7 @@ Proof.
   bdestruct_all; simpl; try lca.
   subst.
   rewrite andb_true_r in H.
-  apply beq_nat_false in H.
+  apply Nat.eqb_neq in H.
   assert (pinv (p x) = pinv (p y)) by auto.
   destruct (Hp x) as [_ [_ [H5 _]]]; auto.
   destruct (Hp y) as [_ [_ [H6 _]]]; auto.
@@ -198,7 +198,7 @@ Proof.
   bdestruct_all; simpl; try lca.
   subst.
   rewrite 2 andb_true_r in H.
-  apply beq_nat_false in H.
+  apply Nat.eqb_neq in H.
   contradiction.
 Qed.
 
@@ -287,7 +287,7 @@ Proof.
   intros z.
   bdestruct_all; simpl; try lca.
   rewrite andb_true_r in H.
-  apply beq_nat_false in H.
+  apply Nat.eqb_neq in H.
   subst z.
   erewrite funbool_to_nat_eq in H2.
   2: { intros. rewrite funbool_to_nat_inverse. reflexivity.
diff --git a/Prelim.v b/Prelim.v
index 6650848..d41e395 100644
--- a/Prelim.v
+++ b/Prelim.v
@@ -14,7 +14,10 @@ Export ListNotations.
 
 (* a lemma that was removed from Coq in 8.16 that I found quite helpful *)
 Lemma le_plus_minus' : forall m n, m <= n -> n = m + (n - m).
-Proof. lia. Qed.
+Proof. intros. rewrite Nat.add_comm. rewrite Nat.sub_add; easy. Qed.
+
+Lemma le_plus_minus_r': forall n m : nat, n <= m -> n + (m - n) = m.
+Proof. intros. rewrite Nat.add_comm. rewrite Nat.sub_add; easy. Qed.
 
 
 
diff --git a/Quantum.v b/Quantum.v
index 661be1f..1f4c1d0 100644
--- a/Quantum.v
+++ b/Quantum.v
@@ -1147,7 +1147,7 @@ Proof.
   distribute_adjoint.
   distribute_scale.
   rewrite UA, Cmult_comm, H. 
-  lma'.
+  lma.
 Qed.
 
 
diff --git a/Rings.v b/Rings.v
index 59fa4e1..32465d6 100644
--- a/Rings.v
+++ b/Rings.v
@@ -1457,7 +1457,7 @@ Proof. unfold Cz8.
        apply injective_projections; simpl; try lra.
        rewrite Rmult_1_r, Rmult_0_l, Rplus_0_r.
        unfold Rdiv.
-       rewrite Rinv_mult_distr, <- Rmult_assoc, Rinv_r. lra.
+       rewrite Rinv_mult, <- Rmult_assoc, Rinv_r. lra.
        all: apply sqrt2_neq_0.
 Qed.
 
diff --git a/VectorStates.v b/VectorStates.v
index 542cdcd..2f9b60e 100644
--- a/VectorStates.v
+++ b/VectorStates.v
@@ -67,7 +67,7 @@ Proof.
   induction n; simpl.
   - Msimpl_light. reflexivity.
   - replace (2^n + (2^n + 0)) with (2^n * 2) by lia.
-    replace (1^n + 0) with (1*1) by (rewrite Nat.pow_1_l, plus_0_r; lia). 
+    replace (1^n + 0) with (1*1) by (rewrite Nat.pow_1_l, Nat.add_0_r; lia). 
     rewrite Nat.pow_1_l.
     rewrite kron_mixed_product.
     rewrite <- IHn.
@@ -445,7 +445,7 @@ Proof.
   reflexivity.
   exists j.
   repeat split; trivial.
-  rewrite <- 2 beq_nat_refl; simpl; lca.
+  rewrite 2 Nat.eqb_refl; simpl; lca.
   intros j' Hj.
   bdestruct_all; auto. 
   all : intros; simpl; try lca.
@@ -646,7 +646,7 @@ Proof.
   repeat rewrite Nat.add_0_r.
   rewrite <- Nat.add_succ_l.
   replace (S (2 ^ n - 1)) with (1 + (2 ^ n - 1)) by easy.
-  rewrite <- le_plus_minus.
+  rewrite <- le_plus_minus'.
   rewrite <- Nat.add_sub_assoc.
   reflexivity.
   all: induction n; simpl; try lia.
@@ -1605,7 +1605,8 @@ Qed.
 Lemma product_0 : forall f n, product (fun _ : nat => false) f n = false.
 Proof.
   intros f n.
-  induction n; simpl; auto.
+  induction n; simpl.
+  reflexivity.
   rewrite IHn; reflexivity.
 Qed.
 
@@ -1729,8 +1730,8 @@ Proof.
   rewrite Mscale_vkron_distr_r.
   apply f_equal2.  
   repeat rewrite <- RtoC_inv by nonzero.
-  rewrite RtoC_pow. 
-  rewrite <- Rinv_pow by nonzero. 
+  rewrite RtoC_pow.
+  rewrite pow_inv by nonzero.
   rewrite <- sqrt_pow by lra. 
   reflexivity.
   apply vkron_to_vsum2.
diff --git a/coq-quantumlib.opam b/coq-quantumlib.opam
index ffb429b..bc8b929 100644
--- a/coq-quantumlib.opam
+++ b/coq-quantumlib.opam
@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "1.2.0"
+version: "1.3.0"
 synopsis: "Coq library for reasoning about quantum programs"
 description: """
 inQWIRE's QuantumLib is a Coq library for reasoning
diff --git a/dune-project b/dune-project
index e80ee42..cecdbce 100644
--- a/dune-project
+++ b/dune-project
@@ -1,6 +1,6 @@
 (lang dune 2.8)
 (name coq-quantumlib)
-(version 1.2.0)
+(version 1.3.0)
 (using coq 0.2)
 
 (generate_opam_files true)