proposition: Fact Zsquare_bound x y : (-y <= x <= y -> x*x <= y*y)%Z.
proof: Proof. intros (H1 & H2). destruct (Z_pos_or_neg x). + apply Z.square_le_mono_nonneg; auto. + replace (y*y)%Z with ((-y)*(-y))%Z by ring. apply Z.square_le_mono_nonpos; lia. Qed.
imports: Arith ZArith Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime php utils_nat) Undecidability.H10.ArithLibs(Zp)