proposition: Lemma to_Z_sub_gt : forall x y, y <=? x = true -> [|x - y|] = ([|x|] - [|y|])%Z.
proof: Proof. intros x y;assert (W:= to_Z_bounded x);assert (W0:= to_Z_bounded y); rewrite leb_spec;intros;rewrite sub_spec, Zmod_small;lia. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz