Skip to content
Snippets Groups Projects
Commit a9167769 authored by Kimaya Bedarkar's avatar Kimaya Bedarkar
Browse files

Apply 1 suggestion(s) to 1 file(s)

parent ffcb6d4d
No related branches found
No related tags found
No related merge requests found
......@@ -101,9 +101,7 @@ Section seq.
Lemma seq_nil n m : seq n m = [] m = 0.
Proof. by destruct m. Qed.
Lemma seq_subseteq m n1 n2 :
n1 n2
seq m n1 seq m n2.
Lemma seq_subseteq_mono m n1 n2 : n1 n2 seq m n1 seq m n2.
Proof. by intros Hle i Hi%elem_of_seq; apply elem_of_seq; lia. Qed.
Lemma Forall_seq (P : nat Prop) i n :
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment