proposition: Lemma le_eq : forall i j, (j <=? i) = true -> (j + 1 <=? i) = false -> i = j.
proof: Proof. intros i j; rewrite leb_spec; destruct (dec_Zle [|j+1|] [|i|]) as [H|H]. rewrite <- leb_spec in H; rewrite H; discriminate. intros H1 _; apply to_Z_inj; rewrite add_spec, to_Z_1 in H. 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 H. lia. split. pose (H3 := to_Z_bounded j); lia. assumption. rewrite H2, Z_mod_same_full in H; elim H; destruct (to_Z_bounded i) as [H3 _]; assumption. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz