Fixes for 8.16

src/CoreData/SemanticCore.v

@@ -256,7 +256,7 @@ Proof.
     rewrite kron_n_assoc; [| auto with wf_db].
     unfold kron.
     destruct (S j mod 2 ^S n) eqn:En.
-    + destruct (Nat.Div0.mod_divides (S j) (2 ^ S n)).
+    + destruct (Nat.mod_divides (S j) (2 ^ S n) (pow2_nonzero _)).
       destruct (H En).
       rewrite H1.
       replace (2 ^ S n * x / 2 ^ S n)%nat with x.
@@ -324,7 +324,7 @@ Proof.
     rewrite Nat.mod_1_r.
     rewrite Nat.div_1_r.
     destruct (S i mod 2 ^ S n) eqn:En.
-    + destruct (Nat.Div0.mod_divides (S i) (2^S n)).
+    + destruct (Nat.mod_divides (S i) (2^S n) (pow2_nonzero _)).
       destruct H; [assumption |].
       rewrite H.
       rewrite Nat.mul_comm.

src/CoreRules/ZXRules.v

@@ -108,7 +108,7 @@ Proof.
 	replace (0)%R with (0 * PI)%R at 1 by lra.
 	replace (0)%R with (INR 0)%R by reflexivity.
 	zxrewrite X_state_copy.
-	rewrite INR_0, Rmult_0_l.
+	rewrite Rmult_0_l.
 	zxrefl.
 Qed.
 
@@ -131,7 +131,7 @@ Proof.
 	replace (0)%R with (0 * PI)%R at 1 by lra.
 	replace (0)%R with (INR 0)%R by reflexivity.
 	zxrewrite Z_state_copy.
-	rewrite INR_0, Rmult_0_l.
+	rewrite Rmult_0_l.
 	zxrefl.
 Qed.
 

src/DiagramRules/Completeness.v

@@ -14,7 +14,7 @@ Proof.
 	rewrite X_2_1_0_semantics.
 	compute_matrix (Z_semantics 0 1 α ⊗ Z_semantics 0 1 (α + PI)).
 	compute_matrix (Z_semantics 0 2 (2 * α + PI)).
-	rewrite <- Cexp_add, <- Rplus_assoc, 3!Cexp_plus_PI, Rplus_diag.
+	rewrite <- Cexp_add, <- Rplus_assoc, 3!Cexp_plus_PI, <- double.
 	prep_matrix_equivalence.
 	by_cell; lca.
 Qed.  

src/DiagramRules/Soundness.v

@@ -52,7 +52,7 @@ Proof.
   - C_field.
   - rewrite Cmod_div by auto.
     rewrite Hmod.
-    rewrite Rdiv_diag; [reflexivity|].
+    apply Rinv_r.
     rewrite Cmod_eq_0_iff.
     auto.
 Qed.

src/Permutations/ZXpermFacts.v

@@ -896,6 +896,8 @@ Lemma zx_of_perm_zxperm n f :
 	ZXperm (zx_of_perm n f).
 Proof.
 	unfold zx_of_perm.
+	rewrite zxperm_iff_cast'.
+	unfold zx_of_perm_uncast.
 	auto_zxperm.
 Qed.