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 2022-11-22 22:46:50 +01:00
parent 64d342bbdf
commit f922960785
1 changed files with 0 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
thue-morse.v
View File

@ -831,27 +831,6 @@ Proof.
reflexivity.
Qed.
Search nth_error.
(*
nth_error_None:
forall [A : Type] (l : list A) (n : nat),
nth_error l n = None <-> length l <= n
nth_error_Some:
forall [A : Type] (l : list A) (n : nat),
nth_error l n <> None <-> n < length l
*)
(*
nth_error_split:
forall [A : Type] (l : list A) (n : nat) [a : A],
nth_error l n = Some a ->
exists l1 l2 : list A, l = l1 ++ a :: l2 /\ length l1 = n
*)
Lemma list_app_length_lt : forall (l l1 l2 : list bool) (b : bool),
l = l1 ++ b :: l2 -> length l1 < length l.
Proof.