proposition: Theorem check_range_correct : forall (v:Z)(r:nat)(rz:Z), (0 < v)%Z -> Z_of_nat (S r) = rz -> check_range v r rz = true -> ~ (exists k:nat, k <= (S r) /\ k <> 1 /\ (exists q:nat, Z.abs_nat v = q*k)).
proof: Proof. intros v r; elim r. - intros rz Hlt H1 H2 Hex; case Hex; intros k; case k. + intros (Hle, (Hne1, (q, Heq))). rewrite Nat.mul_comm in Heq; simpl in Heq. rewrite (Zabs_nat_0 _ Heq) in Hlt. elim (Z.lt_irrefl 0); assumption. + intros k' (Hle, (Hne1, (q, Heq))). inversion Hle. assert (H':k'=0). * assumption. * rewrite H' in Hne1; elim Hne1;auto. * assert (H': S k' <= 0) by assumption. inversion H'. - intros r' Hrec rz Hlt H1 H2 Hex; case Hex; intros k; case k. + intros (Hle, (Hne1, (q, Heq))). rewrite Nat.mul_comm in Heq; simpl in Heq. rewrite (Zabs_nat_0 _ Heq) in Hlt. elim (Z.lt_irrefl 0); assumption. + intros k' (Hle, (Hne1, (q, Heq))). inversion Hle. rewrite <- H1 in H2. rewrite <- (Z_to_nat_and_back v) in H2. assert (Hmod:(Z_of_nat (Z.abs_nat v) mod Z.of_nat (S (S r')) = 0)%Z). * apply verif_divide. replace 0 with (Z.abs_nat 0%Z). apply Zabs_nat_lt. lia. simpl; auto. auto with arith. exists q. assert (H': k' = S r') by assumption. rewrite <- H';auto. * unfold check_range in H2. rewrite Hmod in H2; discriminate H2. * lia. * unfold check_range in H2; fold check_range in H2. case_eq ((v mod rz)%Z). intros Heqmod. rewrite Heqmod in H2. discriminate H2. intros pmod Heqmod; rewrite Heqmod in H2. elim (Hrec (Z.pred rz) Hlt). rewrite <- H1. rewrite inj_S. rewrite inj_S. rewrite inj_S. rewrite <- Zpred_succ. auto. assumption. exists (S k'). repeat split;auto. exists q; assumption. intros p Hmod. elim (Z_mod_lt v rz). rewrite Hmod. unfold Z.le; simpl; intros Hle'; elim Hle';auto. rewrite <- H1. rewrite inj_S. unfold Z.succ. generalize (Zle_0_nat (S r')). intros; lia. Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure Zdiv