proposition: Lemma to_Z_add_1 : forall x y, x <? y = true -> [|x+1|] = ([|x|] + 1)%Z.
proof: Proof. intros x y;assert (W:= to_Z_bounded x);assert (W0:= to_Z_bounded y); rewrite ltb_spec;intros;rewrite add_spec, to_Z_1, Z.mod_small;lia. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz