proposition: Lemma lt_square : forall x y, 0 < x -> x < y -> x*x < y*y.
proof: Proof. intros; apply Z.lt_trans with (x*y). apply Zmult_lt_compat_l;trivial. apply Zmult_lt_compat_r;trivial. lia. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod