proposition: Lemma Zsquare_le x : x <= x*x.
proof: Proof. destruct (Z.lt_ge_cases 0 x). - rewrite <- Z.mul_1_l at 1. rewrite <- Z.mul_le_mono_pos_r; auto with zarith. - pose proof (Z.square_nonneg x); auto with zarith. Qed.
imports: ArithRing ZArith Znumtheory Zpow_facts Lia