1 files changed, 18 insertions, 0 deletions
diff --git a/src/Misc.v b/src/Misc.v
index 24e27c0..66e9b73 100644
--- a/src/Misc.v
+++ b/src/Misc.v
@@ -59,6 +59,18 @@ Proof.
 Qed.
 
 
+Lemma minus_1_lt i : (i == 0) = false -> i - 1 < i = true.
+Proof.
+  intro Hl. rewrite ltb_spec, (to_Z_sub_1 _ 0).
+  - lia.
+  - rewrite ltb_spec. rewrite eqb_false_spec in Hl.
+    assert (0%Z <> [|i|])
+      by (change 0%Z with [|0|]; intro H; apply to_Z_inj in H; auto).
+    destruct (to_Z_bounded i) as [H1 _].
+    clear -H H1. change [|0|] with 0%Z. lia.
+Qed.
+
+
 Lemma foldi_down_ZInd2 :
    forall A (P: Z -> A -> Prop) (f:int -> A -> A) max min a,
    (max < min = true -> P ([|min|])%Z a) ->
@@ -142,6 +154,12 @@ Proof.
   unfold is_true in H2; rewrite ltb_spec, to_Z_0 in H2; pose (H3 := to_Z_bounded i); elimtype False; lia.
 Qed.
 
+Lemma to_list_In_eq : forall {A} (t: array A) i x,
+  i < length t = true -> x = t.[i] -> In x (to_list t).
+Proof.
+  intros A t i x Hi ->. now apply to_list_In.
+Qed.
+
 Lemma In_to_list : forall {A} (t: array A) x,
   In x (to_list t) -> exists i, i < length t = true /\ x = t.[i].
 Proof.