Update
This commit is contained in:
parent
1e18bbe495
commit
836232e28e
@ -169,9 +169,8 @@ Proof.
|
|||||||
assert (incl ([length (l1++l2)]++l2++l1) (l1++[length (l1++l2)]++l2)).
|
assert (incl ([length (l1++l2)]++l2++l1) (l1++[length (l1++l2)]++l2)).
|
||||||
unfold incl. intro a. intro J. rewrite app_assoc in J.
|
unfold incl. intro a. intro J. rewrite app_assoc in J.
|
||||||
rewrite in_app_iff. rewrite in_app_iff in J. destruct J.
|
rewrite in_app_iff. rewrite in_app_iff in J. destruct J.
|
||||||
right. assumption. left. assumption.
|
right. assumption. left. assumption. apply incl_app_inv in H0.
|
||||||
apply incl_app_inv in H0. destruct H0. apply incl_app_inv in H1.
|
destruct H0. apply incl_app_inv in H1. destruct H1.
|
||||||
destruct H1.
|
|
||||||
assert (incl (l1++l2) (l1 ++ [length (l1 ++ l2)] ++ l2)).
|
assert (incl (l1++l2) (l1 ++ [length (l1 ++ l2)] ++ l2)).
|
||||||
apply incl_app; assumption.
|
apply incl_app; assumption.
|
||||||
assert (incl ([length (l1++l2)]++l1++l2) (l1 ++ [length (l1 ++ l2)] ++ l2)).
|
assert (incl ([length (l1++l2)]++l1++l2) (l1 ++ [length (l1 ++ l2)] ++ l2)).
|
||||||
@ -184,11 +183,9 @@ Proof.
|
|||||||
apply incl_app. easy.
|
apply incl_app. easy.
|
||||||
apply perm_seq_1 in H. rewrite app_length in H. simpl in H.
|
apply perm_seq_1 in H. rewrite app_length in H. simpl in H.
|
||||||
rewrite Nat.add_succ_r in H. rewrite seq_S in H. apply incl_app_inv in H.
|
rewrite Nat.add_succ_r in H. rewrite seq_S in H. apply incl_app_inv in H.
|
||||||
destruct H. rewrite app_length at 1. assumption.
|
destruct H. rewrite app_length at 1. assumption. easy. apply Add_app.
|
||||||
easy. apply Add_app.
|
unfold incl in I. unfold permutation. intro k. intro.
|
||||||
unfold incl in I. unfold permutation.
|
apply I. apply in_seq. split. apply Nat.le_0_l. assumption.
|
||||||
intro k. intro. apply I. apply in_seq.
|
|
||||||
split. apply Nat.le_0_l. assumption.
|
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user