proposition: Lemma to_Z_sub_1 : forall x y, y <? x = true -> ([| x - 1|] = [|x|] - 1)%Z.
proof: Proof. intros;apply to_Z_sub_gt. generalize (leb_ltb_trans _ _ _ (leb_0 y) H). rewrite ltb_spec, leb_spec, to_Z_0, to_Z_1;auto with zarith. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz