ModularBaseSystem: finished most admits for addition and multiplication, moved some lemmas to ListUtil.

1 files changed, 11 insertions, 5 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 229fb7488..626a33f02 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -204,15 +204,21 @@ Proof.
   destruct n; auto.
 Qed.
 
-Lemma firstn_app : forall A (l l': list A), firstn (length l) (l ++ l') = l.
+Lemma firstn_app : forall {A} n (xs ys : list A), (n <= length xs)%nat ->
+  firstn n xs = firstn n (xs ++ ys).
 Proof.
-  intros.
-  induction l; simpl; auto.
-  f_equal; auto.
+  induction n; destruct xs; destruct ys; simpl_list; boring; try omega.
+  rewrite (IHn xs (a0 :: ys)) by omega; auto.
 Qed.
-
+    
 Lemma skipn_app : forall A (l l': list A), skipn (length l) (l ++ l') = l'.
 Proof.
   intros.
   induction l; simpl; auto.
 Qed.
+
+Lemma skipn_length : forall {A} n (xs : list A),
+  length (skipn n xs) = (length xs - n)%nat.
+Proof.
+induction n; destruct xs; boring.
+Qed.