relocate and prove an admit

2 files changed, 9 insertions, 8 deletions

diff --git a/.gitmodules b/.gitmodules
index d4861dd59..0a919ab11 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -7,3 +7,4 @@
 [submodule "coqprime"]
 	path = coqprime
 	url = https://github.com/thery/coqprime
+	ignore = dirty
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v
index 8be01866a..95c6929d2 100644
--- a/src/Experiments/SimplyTypedArithmetic.v
+++ b/src/Experiments/SimplyTypedArithmetic.v
@@ -967,6 +967,13 @@ Module Columns.
                | _ => congruence
                end.
       Qed.
+
+      Lemma from_associational_step n t p :
+        from_associational n (t :: p) =
+        cons_to_nth (fst (Positional.place weight t (Nat.pred n)))
+                    (snd (Positional.place weight t (Nat.pred n)))
+                    (from_associational n p).
+      Proof. reflexivity. Qed.
     End FromAssociational.
 
     Section mul.
@@ -1202,13 +1209,6 @@ Module Rows.
         In_cases; subst; auto using length0_nil.
       Qed.
 
-      Lemma Columns_from_associational_step n t p :
-        Columns.from_associational weight n (t :: p) =
-        Columns.cons_to_nth (fst (Positional.place weight t (Nat.pred n)))
-                            (snd (Positional.place weight t (Nat.pred n)))
-                            (Columns.from_associational weight n p).
-      Admitted.
-
       Lemma max_column_size_Columns_from_associational n p :
         n <> 0%nat -> p <> nil ->
         max_column_size (Columns.from_associational weight n p) <> 0%nat.
@@ -1216,7 +1216,7 @@ Module Rows.
         intros.
         rewrite max_column_size_zero_iff.
         intro. destruct p; [congruence | ].
-        rewrite Columns_from_associational_step in *.
+        rewrite Columns.from_associational_step in *.
         cbv [Columns.cons_to_nth] in *.
         match goal with H : forall c, In c (update_nth ?n ?f ?ls) -> _ |- _ =>
                         assert (n < length (update_nth n f ls))%nat;