proposition: Lemma check_s_r_correct : forall s r sqrt, check_s_r s r sqrt = true -> Z_of_N s = 0 \/ ~ isSquare (r * r - 8 * s).
proof: Proof. unfold check_s_r;intros. destruct s as [|s]; trivial;auto. right;CaseEq (square r - xO (xO (xO s)));[intros H1|intros p1 H1| intros p1 H1]; rewrite H1 in H;try discriminate H. elimif. assert (Zpos (xO (xO (xO s))) = 8 * s). repeat rewrite Zpos_xO_add;ring. generalizeclear H1; rewrite H2;mauto;intros. apply (not_square sqrt). simpl Z.of_N; rewrite H1;auto. intros (y,Heq). generalize H1 Heq;mauto. unfold Z_of_N. match goal with |- ?x = _ -> ?y = _ -> _ => replace x with y; try ring end. intros Heq1;rewrite Heq1;intros Heq2. destruct y;discriminate Heq2. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod