proposition: Lemma borned_square : forall x y, 0 <= x -> 0 <= y -> x*x < y*y < (x+1)*(x+1) -> False.
proof: Proof. intros;destruct (Z_lt_ge_dec x y) as [z|z]. assert (x + 1 <= y). lia. assert (0 <= x+1). lia. assert (H4 := le_square _ _ H3 H2). lia. assert (H4 := le_square _ _ H0 (Z.ge_le _ _ z)). lia. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod