Permalink
Browse files

Add PermApp lemma

  • Loading branch information...
norm2782 committed Jun 26, 2012
1 parent 4b48558 commit 3462ef39e62b7eed8b7b42a860c712076e28dac2
Showing with 6 additions and 0 deletions.
  1. +6 −0 src/Properties.v
View
@@ -274,6 +274,12 @@ Lemma NoDupPerm (xs ys : list a) (H : NoDup xs) (p : Permutation xs ys) : NoDup
Qed.
+Lemma PermApp (xs ys zs : list a):
+ Permutation ys zs -> Permutation (xs ++ ys) (xs ++ zs).
+Proof.
+ intros H1.
+ induction xs; [auto | simpl; auto].
+Qed.
Lemma PermutationRotate (xs : list a) : Permutation xs (rotate xs).
induction xs; [constructor | ].

0 comments on commit 3462ef3

Please sign in to comment.