proposition: Lemma minus_1_lt i : (i =? 0) = false -> i - 1 <? i = true.
proof: 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.
imports: Bool List PArray Int63 Ring63 ZArith Psatz