proposition: Lemma Zbounding_square : forall x m, 0 < m -> -m <= x <= m -> x ^ 2 <= m ^ 2.
proof: Proof. intros x m Pm Bx. simpl; unfold Zpower_pos; simpl. rewrite Zmult_assoc. rewrite <- Z.abs_square. apply Z.le_trans with (Z.abs x * m). rewrite <- Zmult_assoc. apply Zmult_le_compat_l; lia. rewrite Zmult_comm. apply Zmult_le_compat_l; lia. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts