baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-10-30 12:57:00 +01:00
parent c8ec0670f8
commit a8d611a276
1 changed files with 18 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
src/subsequences.v
View File

@ -319,6 +319,24 @@ Proof.
rewrite e. rewrite subsequence2_cons_eq. rewrite <- IHl.
rewrite subsequence_cons_eq. split; intro; assumption.
split; intro H. apply subsequence2_cons_l. apply IHl.
destruct H. destruct H. destruct H.
destruct x. destruct x0.
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
simpl in H0. inversion H0. rewrite H2 in n. contradiction n.
reflexivity. inversion H0.
exists x. exists x0. split. assumption.
reflexivity.
apply subsequence_cons_l. apply IHl.
destruct H. destruct H.
destruct x. simpl in H0.
symmetry in H0. apply nil_cons in H0. contradiction H0.
destruct b. simpl in H0. inversion H0. rewrite H2 in n.
contradiction n. reflexivity.
exists x. inversion H. inversion H0.
split; reflexivity.
Qed.