diff --git a/.gitignore b/.gitignore
index a96c72e..681f2ed 100644
--- a/.gitignore
+++ b/.gitignore
@@ -35,3 +35,4 @@ nra.cache
 .DS_Store
 CoqMakefile
 CoqMakefile.conf
+tags
diff --git a/Helpers/DiagonalHelpers.v b/Helpers/DiagonalHelpers.v
index fc7c478..4fd49b6 100644
--- a/Helpers/DiagonalHelpers.v
+++ b/Helpers/DiagonalHelpers.v
@@ -1,4 +1,5 @@
 Require Import QuantumLib.Eigenvectors.
+Require Import QuantumLib.Matrix.
 Require Import MatrixHelpers.
 Require Import GateHelpers.
 
diff --git a/Helpers/MatrixHelpers.v b/Helpers/MatrixHelpers.v
index 73e00d6..71ed94c 100644
--- a/Helpers/MatrixHelpers.v
+++ b/Helpers/MatrixHelpers.v
@@ -82,6 +82,12 @@ Proof.
   unfold diag2, Determinant, big_sum, parity, get_minor; lca.
 Qed.
 
+Lemma Det_diag4 : forall (c1 c2 c3 c4 : C), Determinant (diag4 c1 c2 c3 c4) = c1 * c2 * c3 * c4.
+Proof.
+  intros.
+  unfold diag4, Determinant, big_sum, parity, get_minor; lca.
+Qed.
+
 Lemma row_out_of_bounds: forall {m n} (A : Matrix m n) (i : nat),
   WF_Matrix A -> (i >= m)%nat -> forall (j : nat), A i j = C0.
 Proof.
@@ -593,6 +599,9 @@ Proof.
   apply Coq.Logic.Classical_Prop.or_to_imply.
 Qed.
 
+Definition Mscale_id {n} (x : C) : Square n :=
+  fun i j => if i =? j then x else 0.
+
 Lemma Mscale_access {m n}: forall (a : C) (B : Matrix m n) (i j : nat),
 a * (B i j) = (a .* B) i j.
 Proof.
diff --git a/Helpers/Permutations.v b/Helpers/Permutations.v
index 2916793..adf8ec3 100644
--- a/Helpers/Permutations.v
+++ b/Helpers/Permutations.v
@@ -4,13 +4,364 @@ Require Import QuantumLib.Eigenvectors.
 Require Import Coq.Sets.Ensembles.
 Require Import Coq.Logic.Classical_Pred_Type.
 Require Import Coq.Logic.Classical_Prop.
+Require Import DiagonalHelpers.
+Require Import WFHelpers.
+Require Import UnitaryHelpers.
+Require Import Classical.
+Require Import MatrixHelpers.
 
-Lemma perm_eigenvalues : forall {n} (U D D' : Square n),
+Definition scaled_identity (n : nat) (c : C) : Square n :=
+  fun x y => if (x <? n) && (y <? n)
+             then (if (x =? y) then c else C0)
+             else C0.
+
+(* Define the characteristic polynomial using scaled_identity and Mminus *)
+Definition char_poly {n} (A : Square n) (x : C) : C :=
+  Determinant (Mminus A (scaled_identity n x)).
+
+(* Lemma to show that scaled_identity is well-formed *)
+Lemma WF_scaled_identity : forall {n} (c : C), WF_Matrix (scaled_identity n c).
+Proof.
+  intros n c.
+  unfold WF_Matrix, scaled_identity.
+  intros.
+  destruct (x =? y).
+  destruct H.
+  - (* Case x >= n *)
+    assert (Hlt: (x <? n) = false).
+    { apply Nat.ltb_ge. assumption. }
+    rewrite Hlt.
+    simpl.
+    reflexivity.
+  - (* Case y >= n *)
+    assert (Hlt: (y <? n) = false).
+    { apply Nat.ltb_ge. assumption. }
+    rewrite Hlt.
+    rewrite andb_false_r.
+    reflexivity.
+  - destruct H.
+    assert (Hlt: (x <? n) = false).
+    { apply Nat.ltb_ge. assumption. }
+    rewrite Hlt.
+    simpl.
+    reflexivity.
+    assert (Hlt: (y <? n) = false).
+    { apply Nat.ltb_ge. assumption. }
+    rewrite Hlt.
+    rewrite andb_false_r.
+    reflexivity.
+Qed.
+
+(* Lemma to show that scaled_identity is a complex scalar times the identity *)
+Lemma scaled_identity_eq_scalar_times_identity : forall {n} (x : C),
+  scaled_identity n x = x .* (I n).
+Proof.
+  intros n x.
+  unfold scaled_identity, I.
+  prep_matrix_equality.
+  simpl.
+  destruct ((x0 <? n) && (y <? n)) eqn:E1.
+  - (* Case where both indices are in bounds *)
+    destruct (x0 =? y) eqn:E2.
+    + (* Case where x0 = y *)
+      destruct ((x0 =? y) && (x0 <? n)) eqn:E3.
+      * (* Main case: x0 = y and both in bounds *)
+        unfold scale.
+        rewrite E3.
+        lca.
+      * (* Impossible case - we know x0 = y and x0 < n but E3 is false *)
+        apply andb_true_iff in E1. destruct E1 as [Hx0 Hy].
+        apply Nat.eqb_eq in E2. subst.
+        rewrite Hy in E3.
+        rewrite andb_true_r in E3.
+        rewrite Nat.eqb_refl in E3.
+        discriminate.
+    + (* Case where x0 <> y *)
+      destruct ((x0 =? y) && (x0 <? n)) eqn:E3.
+      * (* Impossible case - we know x0 ≠ y but E3 is true *)
+        apply andb_true_iff in E3.
+        destruct E3 as [Hx0 Hy].
+        rewrite E2 in Hx0.
+        discriminate.
+      * (* Case where indices are different *)
+        unfold scale.
+        rewrite E3.
+        lca.
+  - (* Case where at least one index is out of bounds *)
+    destruct ((x0 =? y) && (x0 <? n)) eqn:E2.
+    + (* Impossible case - we know one index is out but E3 is true *)
+      apply andb_true_iff in E2. destruct E2 as [Hx0 Hy].
+      apply andb_false_iff in E1. destruct E1 as [H1 | H2].
+      * rewrite Hy in H1.
+        discriminate.
+      * apply Nat.eqb_eq in Hx0. subst y.
+        rewrite Hy in H2.
+        discriminate.
+    + unfold scale.
+      rewrite E2.
+      lca.
+Qed.
+
+(* Conjugating a matrix with a unitary preserves the characteristic polynomial *)
+Lemma char_poly_similarity : forall {n} (A B U : Square n) x,
+  WF_Unitary U -> U × A × U† = B -> char_poly A x = char_poly B x.
+Proof.
+  intros n A B U x WF_U H_conj.
+  unfold char_poly.
+  assert (H_eq : Mminus B (scaled_identity n x) = 
+                 U × (Mminus A (scaled_identity n x)) × U†).
+{
+  unfold Mminus.
+  (* First show that U × (scaled_identity n x) = (scaled_identity n x) × U *)
+  assert (H_comm : U × (scaled_identity n x) = (scaled_identity n x) × U).
+  {
+    rewrite scaled_identity_eq_scalar_times_identity.
+    rewrite Mscale_mult_dist_r.
+    rewrite Mscale_mult_dist_l.
+    rewrite Mmult_1_r.
+    rewrite Mmult_1_l.
+    reflexivity.
+    solve_WF_matrix.
+    solve_WF_matrix.
+  }
+  (* Now use distributive properties *)
+  rewrite <- H_conj.
+  rewrite Mmult_plus_distr_l.
+  rewrite Mmult_plus_distr_r.
+  assert (H_comm_mopp: U × Mopp(scaled_identity n x) = Mopp(scaled_identity n x) × U).
+  {
+    unfold Mopp.
+    rewrite Mscale_mult_dist_r.
+    rewrite Mscale_mult_dist_l.
+    rewrite H_comm.
+    reflexivity.
+  }
+  rewrite H_comm_mopp.
+  rewrite Mmult_assoc.
+  rewrite Mmult_assoc.
+  rewrite other_unitary_decomp.
+  Msimpl.
+  reflexivity.
+  - unfold Mopp at 1.
+    apply WF_scale.
+    apply WF_scaled_identity.
+  - solve_WF_matrix.
+}
+rewrite H_eq.
+rewrite <- Determinant_multiplicative.
+rewrite <- Determinant_multiplicative.
+rewrite <- Cmult_assoc.
+rewrite <- Cmult_comm.
+rewrite <- Cmult_assoc.
+assert (H_unit1: U × U† = I n) by (apply other_unitary_decomp; auto).
+assert (H_det: Determinant (U × U†) = Determinant (I n)) by (rewrite H_unit1; reflexivity).
+rewrite Determinant_multiplicative.
+assert (H_unit2: U† × U = I n).
+{
+  destruct WF_U as [WF_U unit_U].
+  apply unit_U.
+}
+rewrite H_unit2.
+rewrite Det_I.
+rewrite Cmult_1_r.
+reflexivity.
+Qed.
+
+Fixpoint prod_f (f : nat -> C) (n : nat) : C :=
+  match n with
+  | 0 => C1 (* The product over an empty range is 1 *)
+  | S n' => (f n') * (prod_f f n') (* Multiply the current value with the rest *)
+  end.
+
+(* Helper lemma: For diagonal matrices, off-diagonal entries are 0 *)
+(* Lemma diagonal_off_diag_zero : forall {n} (D : Square n),
+  WF_Diagonal D -> forall i j, i <> j -> D i j = C0.
+Proof.
+  intros n D [WF_D D_diag] i j Hij.
+  apply D_diag.
+  assumption.
+Qed.
+
+(* Helper lemma: For diagonal matrices, diagonal entries are well-defined *)
+Lemma diagonal_diag_well_defined : forall {n} (D : Square n),
+  WF_Diagonal D -> forall i, (i < n)%nat -> exists c, D i i = c.
+Proof.
+  intros n D [WF_D D_diag] i Hi.
+  destruct (classic (D i i = C0)).
+  - exists C0. assumption.
+  - exists (D i i). reflexivity.
+Qed. *)
+
+(* Helper lemma: Product of diagonal entries equals determinant *)
+Lemma diagonal_det_prod : forall (D : Square 4),
+  WF_Diagonal D -> Determinant D = prod_f (fun i => D i i) 4.
+Proof.
+  intros D WF_D.
+  unfold prod_f.
+  Csimpl.
+  assert (H: exists c1 c2 c3 c4, D = diag4 c1 c2 c3 c4).
+  {
+    exists (D 0%nat 0%nat), (D 1%nat 1%nat), (D 2%nat 2%nat), (D 3%nat 3%nat).
+    destruct WF_D as [WF_D D_diag].
+    prep_matrix_equality.
+    destruct x, y; try reflexivity.
+    try (apply D_diag; lia).
+    Msimpl.
+    assert (H_neq: (S x) <> 0%nat).
+    { apply Nat.neq_succ_0. }
+    rewrite D_diag by auto.
+    unfold diag4.
+    destruct x.
+    reflexivity.
+    destruct x.
+    reflexivity.
+    destruct x.
+    reflexivity.
+    destruct x.
+    reflexivity.
+    reflexivity.
+    destruct x, y.
+    - simpl. unfold diag4. reflexivity.
+    - rewrite D_diag by auto.
+      unfold diag4.
+      reflexivity.
+    - rewrite D_diag by auto.
+      unfold diag4.
+      destruct x.
+      reflexivity.
+      destruct x.
+      reflexivity.
+      reflexivity.
+    - destruct x, y.
+      simpl. unfold diag4. reflexivity.
+      rewrite D_diag by lia.
+      unfold diag4.
+      reflexivity.
+      rewrite D_diag by lia.
+      unfold diag4.
+      destruct x.
+      reflexivity.
+      reflexivity.
+      destruct x, y; simpl.
+      reflexivity.
+      simpl.
+      unfold diag4.
+      rewrite D_diag by lia.
+      reflexivity.
+      unfold diag4.
+      rewrite D_diag by lia.
+      reflexivity.
+      simpl.
+      assert (H_bound: ((S (S (S (S x)))) >= 4)%nat) by lia.
+      rewrite (row_out_of_bounds D _).
+      unfold diag4.
+      reflexivity.
+      assumption.
+      assumption.
+  }
+  destruct H as [c1 [c2 [c3 [c4 D_eq]]]].
+  rewrite D_eq.
+  rewrite Det_diag4.
+  unfold diag4.
+  repeat rewrite Cmult_assoc.
+  lca.
+Qed.
+
+Lemma char_poly_diagonal : forall (D : Square 4),
+  WF_Diagonal D -> forall x, char_poly D x = prod_f (fun i => D i i - x) 4.
+Proof.
+intros D WF_D x.
+unfold char_poly.
+assert (H_diag: WF_Diagonal (Mminus D (scaled_identity 4 x))).
+{
+  rewrite scaled_identity_eq_scalar_times_identity.
+  unfold Mminus.
+  unfold Mopp.
+  unfold WF_Diagonal.
+  split. solve_WF_matrix.
+  destruct WF_D as [WF_D D_diag].
+  intros i j H_neq.
+  rewrite Mplus_access.
+  rewrite D_diag.
+  rewrite Cplus_0_l.
+  rewrite <- Mscale_access.
+  rewrite <- Mscale_access.
+  unfold I.
+  destruct (i =? j) eqn:Eij.
+  - apply Nat.eqb_eq in Eij.
+    contradiction.
+  - simpl.
+    lca.
+  - assumption.
+}
+rewrite (diagonal_det_prod (Mminus D (scaled_identity 4 x))); auto.
+rewrite scaled_identity_eq_scalar_times_identity.
+unfold Mminus.
+unfold Mopp.
+lca.
+Qed.
+
+Lemma poly_roots_perm : forall (f g : nat -> C),
+  (forall x, prod_f (fun i => f i - x) 4 = prod_f (fun i => g i - x) 4) ->
+  exists (σ : nat -> nat), permutation 4 σ /\ forall (i : nat), f i = g (σ i).
+Proof.
+  intros f g H_prod.
+  assert (H_exists : forall i, (i < 4)%nat -> exists j, (j < 4)%nat /\ f i = g j).
+  {
+    admit.
+  }
+  (* For each i < 4, get the j that H_exists guarantees *)
+  destruct (H_exists 0%nat) as [j0 [H_j0 H_eq0]]. { auto. }
+  destruct (H_exists 1%nat) as [j1 [H_j1 H_eq1]]. { auto. }
+  destruct (H_exists 2%nat) as [j2 [H_j2 H_eq2]]. { auto. }
+  destruct (H_exists 3%nat) as [j3 [H_j3 H_eq3]]. { auto. }
+
+  (* Define our permutation σ *)
+  exists (fun i => match i with
+                  | 0 => j0
+                  | 1 => j1
+                  | 2 => j2
+                  | 3 => j3
+                  | _ => i
+                  end).
+  split.
+Admitted.
+
+Lemma perm_eigenvalues : forall (U D E : Square 4),
+  WF_Unitary U -> WF_Diagonal D -> WF_Diagonal E -> U × D × U† = E ->
+  exists (σ : nat -> nat),
+    permutation 4 σ /\ forall (i : nat), D i i = E (σ i) (σ i).
+Proof.
+  intros U D E WF_U WF_D WF_E H_conj.
+  
+  assert (Hchar : forall x, char_poly D x = char_poly E x).
+  {
+    intros x.
+    apply (char_poly_similarity D E U x); assumption.
+  }
+  
+  assert (Hprod : forall x : C, prod_f (fun i => D i i - x) 4 = prod_f (fun i => E i i - x) 4).
+  {
+    intros x.
+    rewrite <- (char_poly_diagonal D WF_D x).
+    rewrite <- (char_poly_diagonal E WF_E x).
+    apply Hchar.
+  }
+
+  apply poly_roots_perm in Hprod.
+  destruct Hprod as [σ [Hperm Heq]].
+  exists σ.
+  split. assumption.
+  intros i.
+  apply Heq.
+Qed.
+
+(* Lemma perm_eigenvalues : forall {n} (U D D' : Square n),
   WF_Unitary U -> WF_Diagonal D -> WF_Diagonal D' -> U × D × U† = D' ->
   exists (σ : nat -> nat),
     permutation n σ /\ forall (i : nat), D i i = D' (σ i) (σ i).
 Proof.
-Admitted.
+Admitted. *)
 
 (* To equate the eigenvalues of two matrices, we often need equality of matrices
    up to some permutation. This lemma allows us to take the existence of a
diff --git a/Helpers/PolynomialHelpers.v b/Helpers/PolynomialHelpers.v
new file mode 100644
index 0000000..64873c7
--- /dev/null
+++ b/Helpers/PolynomialHelpers.v
@@ -0,0 +1,349 @@
+Require Import QuantumLib.Complex.
+Require Import QuantumLib.Polynomial.
+Require Import QuantumLib.Matrix.
+Require Import QuantumLib.Quantum.
+Require Import QuantumLib.Eigenvectors.
+Require Import QuantumLib.Permutations.
+Require Import MatrixHelpers.
+Require Import DiagonalHelpers.
+Require Import UnitaryHelpers.
+Require Import Permutations.
+Require Import Setoid.
+
+Module P := Polynomial.
+
+(* Open the polynomial scope *)
+Local Open Scope poly_scope.
+
+(* Define a function to create a polynomial with a root at a given point *)
+Definition linear_poly (c : C) : Polynomial := [- c; C1].
+
+(* Define a function to create a polynomial (x - c) *)
+Definition x_minus_c (c : C) : Polynomial := linear_poly c.
+
+(* Define a function to create a polynomial (c - x) *)
+Definition c_minus_x (c : C) : Polynomial := [c; -C1].
+
+(* A collection of linear factors *)
+Definition Factors := list C.
+
+Fixpoint poly_prod (c : Factors) : Polynomial :=
+  match c with
+  | nil    => [C1]
+  | h :: t => [h; -C1] *, poly_prod t
+  end.
+
+(* Lemma 1.1 *)
+Lemma complex_poly_degree : forall (q : Polynomial) (d : C),
+    Peval ([d; -C1] *, q) <> Peval [C1].
+Proof.
+  intros q d Heq'.
+  apply degree_mor in Heq' as Hdeg.
+  assert (Heq : ([d; - C1] *, q) ≅ [C1]) by apply Heq'.
+  unfold degree at 2 in Hdeg.
+  unfold compactify in Hdeg.
+  simpl length in Hdeg.
+  destruct (Ceq_dec C1 C0) as [H01 | _]; try (inversion H01; lra).
+  simpl rev in Hdeg.
+  assert (H_nil_neq_1 : ~ ([] ≅ [C1])).
+  { intro H_nil_1.
+    assert ([][[0]] = [C1][[0]]) by now rewrite H_nil_1.
+    unfold Peval in H; simpl in H.
+    inversion H; lra. }
+  assert (Hq_neq_nil : ~ (q ≅ [])).
+  { intro H_qnil.
+    setoid_rewrite H_qnil in Heq.
+    now rewrite P.Pmult_0_r in Heq. }
+  assert (Hdx_neq_nil : ~ ([d; - C1] ≅ [])).
+  { intro H_dxnil.
+    setoid_rewrite H_dxnil in Heq.
+    now simpl in Heq. }
+  rewrite (Pmult_degree _ _ Hdx_neq_nil Hq_neq_nil) in Hdeg.
+
+  unfold degree at 1 in Hdeg.
+  unfold compactify in Hdeg.
+  simpl in Hdeg.
+  destruct (Ceq_dec (-C1) 0) as [H01 | _]; try (inversion H01; lra).
+  simpl in Hdeg. lia.
+Qed.
+
+(* Lemma 1.2 (Euclid's Lemma) *)
+Lemma euclid_lemma : forall {d e : C} {p r : Polynomial},
+  [d; -C1] *, p ≅ r *, [e; -C1] ->
+  d = e \/ exists (q : Polynomial), [d; -C1] *, q ≅ r.
+Proof.
+  (* TODO: the polynomial theorem names collide with Coq.PArith *)
+
+  intros d e p r Heq.
+  destruct (Ceq_dec d e) as [| Hneq]; [auto | right].
+  apply Cminus_eq_contra in Hneq.
+
+  (* construct 1/(d - e) * (r - p) *)
+  exists ([/ (d - e)] *, (r +, -,p)).
+  rewrite P.Pmult_comm.
+  rewrite P.Pmult_assoc.
+  rewrite P.Pmult_plus_distr_r.
+  rewrite P.Pmult_comm in Heq.
+  unfold Popp.
+  rewrite P.Pmult_assoc, Heq.
+  rewrite <- P.Pmult_assoc.
+  rewrite (P.Pmult_comm ([-C1])).
+  rewrite P.Pmult_assoc.
+  rewrite <- (P.Pmult_plus_distr_l r).
+  simpl P.Pplus.
+  replace (d + (((- C1) * e) + 0)) with (d - e) by lca.
+  replace ((- C1) + ((- C1) * (- C1))) with C0 by lca.
+  rewrite (p_Peq_compactify_p [d - e; C0]).
+
+  unfold compactify.
+  simpl prune.
+  destruct (Ceq_dec 0 0); try easy.
+  destruct (Ceq_dec (d - e) 0); try easy.
+  simpl rev.
+
+  rewrite (P.Pmult_comm r), <- P.Pmult_assoc.
+  simpl P.Pmult at 2; rewrite Cplus_0_r.
+  rewrite (Cinv_l _ Hneq).
+  apply Pmult_1_l.
+Qed.
+
+(* Lemma 1.3 *)
+Lemma poly_isolate_factor : forall (d : C) (facs : list C),
+    facs <> [] ->
+    (forall (p : Polynomial),
+      [d; -C1] *, p ≅ poly_prod facs ->
+      exists (k : nat), nth_error facs k = Some d).
+Proof.
+  intros d facs.
+  induction facs as [| f facs IH]; try contradiction.
+  destruct facs as [| f0 facs].
+  - (* singleton list *)
+    intros _ p0 Heq. clear IH.
+    exists 0%nat.
+    simpl in *.
+
+    repeat rewrite Cplus_0_r in Heq.
+    repeat rewrite Cmult_1_r in Heq.
+
+    rewrite <- (Pmult_1_l [f; -C1]) in Heq.
+    destruct (euclid_lemma Heq) as [ Hdf | [q Hex] ]; try (subst; auto).
+    now apply complex_poly_degree in Hex.
+
+  - intros _ p0 Heq.
+    specialize (IH ltac:(easy)).
+    setoid_replace
+      (poly_prod (f :: f0 :: facs)) with
+      ([f; -C1] *, poly_prod (f0 :: facs))
+      using relation Peq in Heq.
+    2: {
+      unfold poly_prod.
+      now repeat rewrite <- P.Pmult_assoc.
+    }
+    unfold poly_prod in *.
+    fold poly_prod in *.
+    rewrite (P.Pmult_comm [f; -C1]) in Heq.
+    destruct (euclid_lemma Heq) as [ Hdf | [q Hex] ].
+    + exists 0%nat.
+      subst. auto.
+    + destruct (IH q Hex) as [k Hk].
+      exists (S k).
+      auto.
+Qed.
+
+Lemma singleton_list : forall {T} {l : list T},
+  (length l = 1)%nat -> exists x, l = [x].
+Proof.
+  intros.
+  destruct l; try inversion H.
+  destruct l; try inversion H1.
+  now exists t.
+Qed.
+
+Lemma poly_prod_middle : forall (l1 l2 : Factors) (f : C), poly_prod (l1 ++ f :: l2) ≅ poly_prod (f :: l1 ++ l2).
+Proof.
+  intro l1.
+  induction l1; try reflexivity.
+  intros l2 f.
+  simpl app.
+  unfold poly_prod; fold poly_prod.
+  rewrite IHl1.
+  unfold poly_prod; fold poly_prod.
+  do 2 rewrite <- P.Pmult_assoc.
+  now rewrite (P.Pmult_comm [a; -C1] [f; -C1]).
+Qed.
+
+Lemma Pmult_0_factor : forall (p1 p2 : Polynomial),
+  (p1 *, p2) ≅ [] -> p1 ≅ [] \/ p2 ≅ [].
+Proof.
+  intros p1 p2 H.
+  destruct (Peq_0_dec p1), (Peq_0_dec p2); try auto.
+  destruct (Pmult_neq_0 _ _ n n0); auto.
+Qed.
+
+(* Lemma 1.4 *)
+Lemma Pfac_cancel_l : forall (d : C) (p1 p2 : Polynomial),
+    [d; -C1] *, p1 ≅ [d; -C1] *, p2 -> p1 ≅ p2.
+Proof.
+  intros d p1 p2 Hnil.
+  pose proof (H := Pplus_mor _ _ Hnil ([d; -C1] *, -, p2) _ ltac:(reflexivity)).
+  rewrite <- P.Pmult_plus_distr_l in H.
+  unfold Popp in H.
+  rewrite <- P.Pmult_assoc in H.
+  rewrite (P.Pmult_comm [d; -C1] [- C1]) in H.
+  rewrite P.Pmult_assoc in H.
+  rewrite Pplus_opp_r in H.
+  destruct (Pmult_0_factor _ _ H).
+  - apply degree_mor in H0. unfold degree in H0.
+    unfold compactify in H0.
+    simpl in H0.
+    destruct (Ceq_dec (-C1) 0%R) as [H01 | _]; try (inversion H01; lra).
+    simpl in H0. lia.
+  - pose proof (H' := Pplus_mor _ _ H0 p2  _ ltac:(reflexivity)).
+    rewrite P.Pplus_assoc in H'.
+    setoid_replace ([-C1] *, p2 +, p2) with
+      ([] : Polynomial) in H' by now rewrite Pplus_opp_l.
+    simpl in H'. now rewrite P.Pplus_0_r in H'.
+Qed.
+
+(* Lemma 1.5 *)
+Lemma roots_equal_implies_permutation :
+  forall (n : nat),
+  (n > 0)%nat ->
+  forall (ds es: list C),
+  length ds = n -> length es = n ->
+  (poly_prod ds ≅ poly_prod es) ->
+  exists f, permutation n f /\ (forall i, ds !! i = es !! f i).
+Proof.
+  intros n.
+  induction n; try lia.
+  (* intros. *)
+  intros H ds es Hdlen Helen Hpeq.
+  destruct n as [| n].
+  - exists idn.
+    split.
+    + (* Permutation *)
+      apply idn_permutation.
+    + (* perm_pair_eq *)
+      destruct (singleton_list Hdlen) as [delem Hd].
+      destruct (singleton_list Helen) as [eelem He].
+      subst.
+      destruct i.
+      * unfold poly_prod in Hpeq.
+        simpl; f_equal.
+        simpl in Hpeq.
+        apply Peq_head_eq in Hpeq.
+        (* Why can't we use lca here? *)
+        repeat rewrite Cplus_0_r in Hpeq.
+        repeat rewrite Cmult_1_r in Hpeq.
+        auto.
+      * easy.
+  - remember (S n) as N. clear H.
+    specialize (IHn ltac:(lia)).
+    destruct ds as [| d ds]; try easy.
+    assert (Heneqnil : es <> []).
+    { intro Hcontra.
+      subst. easy. }
+    destruct (poly_isolate_factor d es Heneqnil (poly_prod ds) Hpeq) as [k Hk].
+    assert (Hk_le_n : (k < S N)%nat).
+    { rewrite <- Helen.
+      rewrite <- nth_error_Some.
+      now rewrite Hk. }
+    clear Heneqnil.
+
+    (* break 'es' into multiple pieces *)
+    destruct (nth_error_split es k Hk) as [e1 [e2 [Hcombine Hidx] ] ].
+    rewrite Hcombine in Hpeq.
+
+    rewrite poly_prod_middle in Hpeq.
+    unfold poly_prod in Hpeq. fold poly_prod in Hpeq.
+
+    assert (Hleneq : length (e1 ++ e2) = N).
+    { subst.
+      rewrite app_length in *.
+      simpl in *.
+      lia. }
+
+    specialize (IHn ds (e1 ++ e2) ltac:(auto) Hleneq).
+
+    assert (Hpeq' : poly_prod ds ≅ poly_prod (e1 ++ e2)).
+    { now apply Pfac_cancel_l in Hpeq. }
+    clear Hpeq.
+
+    destruct (IHn ltac:(easy)) as [f' [Hperm Hpermeq] ].
+
+    pose (f := fun i =>
+              match i with
+              | 0 => k
+              | S i' =>
+                  let j := f' i' in
+                  if j <? k then j else S j
+              end).
+
+    exists f.
+
+    split.
+    { destruct Hperm as [f'inv Hf'inv].
+
+      pose (finv := fun j =>
+                if j =? k then 0%nat else
+                  if j <? k then S (f'inv j)
+                  else S (f'inv (pred j))).
+      exists finv.
+      intros x Hx.
+      repeat split.
+      - (* f x < S (S n) *)
+        destruct x.
+        + unfold f. subst.
+          rewrite app_length in Helen.
+          simpl in Helen.
+          lia.
+        + specialize (Hf'inv x ltac:(lia)).
+          simpl. destruct (f' x <? k) eqn:E; lia.
+      - (* finv x < S (S n) *)
+        unfold finv.
+        bdestruct_all; try (rewrite <- Nat.succ_lt_mono).
+        + (* k <= N *)
+          now destruct (Hf'inv x ltac:(lia)).
+        + lia.
+        + (* f'inv (pred x) < N *)
+          destruct x; simpl.
+          * now destruct (Hf'inv 0%nat ltac:(lia)).
+          * now destruct (Hf'inv x ltac:(lia)).
+      - (* finv (f x) = x *)
+        unfold finv, f.
+        destruct x.
+        + (* x = 0 *)
+          simpl.
+          bdestruct (k =? k); [ lia | easy ].
+        + bdestruct_all; simpl; destruct (Hf'inv x ltac:(lia)); lia.
+      - (* f (finv x) = x *)
+        unfold finv, f.
+        destruct x.
+        + bdestruct_all; try (destruct (Hf'inv 0%nat ltac:(lia))); lia.
+        + bdestruct_all.
+          * destruct (Hf'inv (S x) ltac:(lia)). lia.
+          * destruct (Hf'inv (S x) ltac:(lia)). lia.
+          * auto.
+          * simpl in *. destruct (Hf'inv x ltac:(lia)). lia.
+          * destruct (Hf'inv x ltac:(lia)). simpl. lia.
+    }
+
+    unfold permutation.
+    intros i.
+    destruct i as [| i']; try auto.
+    subst.
+    simpl.
+    rewrite Hpermeq.
+    bdestruct (f' i' <? length e1)%nat.
+    + do 2 rewrite (nth_error_app1 _ _ H); reflexivity.
+    + replace (e1 ++ d :: e2) with ((e1 ++ [d]) ++ e2)
+        by ( rewrite <- app_assoc; auto ).
+      assert (Hsecond : (length (e1 ++ [d]) <= S (f' i'))%nat).
+      { rewrite app_length. simpl. lia. }
+      rewrite (nth_error_app2 _ _ H).
+      rewrite (nth_error_app2 _ _ Hsecond).
+      rewrite app_length.
+      simpl length.
+      rewrite Nat.add_1_r.
+      auto.
+Qed.
diff --git a/flake.nix b/flake.nix
index e3b1128..347bfb3 100644
--- a/flake.nix
+++ b/flake.nix
@@ -15,7 +15,7 @@
       system = "x86_64-linux";
       pkgs = nixpkgs.legacyPackages.${system};
       pkgs-unstable = nixpkgs-unstable.legacyPackages.${system};
-      coq-quantumlib-version = "v1.4.0";
+      coq-quantumlib-version = "v1.6.0";
     in
     let
       coq-quantumlib = pkgs.coqPackages.mkCoqDerivation {
@@ -25,8 +25,8 @@
 
         defaultVersion = coq-quantumlib-version;
         release.${coq-quantumlib-version} = {
-          rev = "80018571961e13968bfd80ea9cb061d9469b0817";
-          sha256 = "sha256-mx74GxIwF6mgmrELmNl0l3GiBBf/WrpouHfszylhTYQ=";
+          rev = "5e0e4da5e64fcf9b4390a274748079ed270c1965";
+          sha256 = "sha256-eKKYWUj6zDh48J5mahOr+HwWULgfn3K/3TY3oFhhYJA=";
         };
         useDune = true;
       };