proposition: Lemma square_bound : forall x m, -m <= x <= m -> x * x <= m * m.
proof: Proof. intros x m Bx. assert (Pm : 0 <= m) by lia. rewrite <- Z.abs_square. apply Z.le_trans with (Z.abs x * m). apply Zmult_le_compat_l; auto with *; try lia. apply Zmult_le_compat_r; auto with *; try lia. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts