proposition: Lemma le_square : forall x y, 0 <= x -> x <= y -> x*x <= y*y.
proof: Proof. intros; apply Z.le_trans with (x*y). apply Zmult_le_compat_l;trivial. apply Zmult_le_compat_r;trivial. lia. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod