proposition: Lemma lt_eq : forall i j, (i <? j + 1) = true -> (i <? j) = false -> i = j.
proof: Proof. intros i j. rewrite ltb_spec. destruct (dec_Zlt [|i|] [|j|]) as [H|H]. rewrite <- ltb_spec in H; rewrite H; discriminate. intros H1 _; apply to_Z_inj. rewrite add_spec in H1. rewrite to_Z_1 in H1. assert (H2: (([|j|] + 1)%Z < wB)%Z \/ ([|j|] + 1)%Z = wB). pose (H3 := to_Z_bounded j); lia. destruct H2 as [H2|H2]. rewrite Z.mod_small in H1. lia. split. pose (H3 := to_Z_bounded j); lia. assumption. rewrite H2, Z_mod_same_full in H1; elimtype False. destruct (to_Z_bounded i) as [H3 _]. lia. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz