proposition: Lemma square_bound_opp : forall x m, m <= x <= -m -> x * x <= m * m.
proof: Proof. intros x m Bx. rewrite <- (Zmult_opp_opp m m). apply square_bound; auto with *. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts