proposition: Theorem Nprime_least_div_ge_p : forall n p, S n < p -> Nprime p -> Nleast_div_ge n p = p.
proof: Proof. induction n. intros. compute. auto. intros. destruct H0. apply le_le_S_eq in H. destruct H. simpl. assert(~(p-S n|p)). apply H1. split. apply (Nat.sub_le_mono_r (S(S(S(S n)))) p (S n)) in H. rewrite Nat.sub_succ_l in H. rewrite Nat.sub_succ_l in H. rewrite Nat.sub_succ_l in H. rewrite Nat.sub_diag in H. auto with arith. auto. auto. auto with arith. apply Nat.sub_lt. apply Nat.le_trans with (S(S(S n))). auto with arith. auto. auto with arith. auto with arith. assert (~Ndiv_algo (p-S n) p=true). intro. apply H1 with (p-S n). split. apply (Nat.sub_le_mono_r (S(S(S(S n)))) p (S n)) in H. rewrite Nat.sub_succ_l in H. rewrite Nat.sub_succ_l in H. rewrite Nat.sub_succ_l in H. rewrite Nat.sub_diag in H. auto with arith. auto. auto. auto. apply Nat.sub_lt. apply Nat.le_trans with (S(S(S(S n)))). auto. auto. auto with arith. apply Ndiv_algo_complete. unfold gt. apply (Nat.sub_le_mono_r (S(S(S(S n)))) p (S n)) in H. rewrite Nat.sub_succ_l in H. rewrite Nat.sub_succ_l in H. rewrite Nat.sub_succ_l in H. rewrite Nat.sub_diag in H. apply Nat.le_trans with 3. auto. auto. auto. auto. auto. auto. auto with arith. destruct (Ndiv_algo (p-S n) p). contradiction H3. auto. apply IHn. apply Nat.le_trans with (S(S(S(S n)))). auto. auto. split. auto. auto. destruct p. inversion H. destruct p. inversion H. destruct p. inversion H. do 3 apply eq_add_S in H. rewrite H. unfold Nleast_div_ge. rewrite Nat.sub_succ_l. rewrite Nat.sub_succ_l. rewrite Nat.sub_diag. assert(~(Ndiv_algo 2 (S(S(S p)))=true)). intro. apply H1 with 2. split. auto. auto with arith. apply Ndiv_algo_complete. auto. auto. destruct (Ndiv_algo 2 (S(S(S p)))). contradiction H2. auto. fold Nleast_div_ge. rewrite <- H. apply IHn. auto. split. auto with arith. rewrite H. auto. auto. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)