proposition: Theorem check_correct : forall p:nat, 0 < p -> check_primality p = true -> ~(exists k:nat, k <> 1 /\ k <> p /\ (exists q:nat, p = q*k)).
proof: Proof. unfold lt; intros p Hle; elim Hle. - intros Hcp (k, (Hne1, (Hne1bis, (q, Heq)))); rewrite Nat.mul_comm in Heq. assert (Hle' : k < 1). + elim (proj1 (Nat.lt_eq_cases k 1)); try(intuition; fail). apply divisor_smaller with (2:= Heq); auto. + case_eq k. * intros Heq'; rewrite Heq' in Heq; simpl in Heq; discriminate Heq. * intros; lia. - intros p' Hlep' Hrec; unfold check_primality. assert (H':(exists p'':nat, p' = (S p''))). + inversion Hlep'. * exists 0; auto. * eapply ex_intro;eauto. + elim H'; intros p'' Hp''; rewrite Hp''. repeat rewrite <- pred_Sn. intros Hcr Hex; elim check_range_correct with (3:= Hcr). * rewrite inj_S; generalize (Zle_0_nat (S p'')). intros; lia. * auto. * elim Hex; intros k (Hne1, (HneSSp'', (q, Heq))); exists k. split. assert (HkleSSp'': k <= S (S p'')). apply (divisor_smaller (S (S p'')) q); auto with arith. rewrite Nat.mul_comm; assumption. lia. split. assumption. exists q; now rewrite nat_to_Z_and_back. Qed.
imports: ZArith Arith Lia