proposition: Theorem Ngreatest_least_div_relation : forall n, n > 2 -> (Ngreatest_div n) * (Nleast_div n)=n.
proof: Proof. intros. assert(Nprime n \/ ~Nprime n). apply Nprime_or_not_prime. destruct H0. replace (Ngreatest_div n) with 1. replace (Nleast_div n) with n. ring. symmetry. apply Nprime_least_div_p. auto. symmetry. apply Nprime_greatest_div_1. auto. assert(Q:~Nprime n). auto. clear H0. assert((Ngreatest_div n)*(Nleast_div n)<=n). assert((Ngreatest_div n)|n). apply Ngreatest_div_div. auto with arith. destruct H0. assert(q|n). exists (Ngreatest_div n). rewrite Nat.mul_comm. auto. apply Nleast_div_least in H1. rewrite H0 at 3. rewrite Nat.mul_comm. apply Nat.mul_le_mono_r. auto. auto with arith. destruct q. rewrite Nat.mul_0_l in H0. rewrite H0 in H. inversion H. destruct q. rewrite Nat.mul_1_l in H0. assert(Ngreatest_div n<n). apply Ngreatest_div_lt_p. auto with arith. rewrite <- H0 in H2 at 1. apply Nat.lt_irrefl in H2. contradiction. auto with arith. assert(q<=n). apply Ndiv_le; auto. destruct n. inversion H. auto with arith. apply le_le_S_eq in H2. destruct H2. auto. rewrite H2 in H0. destruct n. inversion H. assert(1<=Ngreatest_div (S n)). apply Ngreatest_div_le_1. apply le_le_S_eq in H3. destruct H3. replace q with (q*1). rewrite H0. rewrite H2. apply Nat.mul_lt_mono_pos_l; [apply Nat.lt_0_succ|]. auto. ring. symmetry in H3. apply Ngreatest_div_1_prime in H3. apply Q in H3. contradiction. auto with arith. assert((Ngreatest_div n)*(Nleast_div n)>=n). assert((Nleast_div n)|n). apply Nleast_div_div. auto with arith. destruct H1. assert(q|n). exists (Nleast_div n). rewrite Nat.mul_comm. auto. apply Ngreatest_div_greatest in H2. unfold ge. rewrite H1 at 1. apply Nat.mul_le_mono_r. auto. auto with arith. destruct q. rewrite Nat.mul_0_l in H1. rewrite H1 in H. inversion H. auto with arith. apply Ndiv_le in H2. apply le_le_S_eq in H2. destruct H2. auto. rewrite H2 in H1. assert(Nleast_div n>=2). apply Nleast_div_ge_2. destruct n. inversion H. auto with arith. replace q with (q*1). rewrite H1. rewrite H2. destruct n. inversion H. apply Nat.mul_lt_mono_pos_l; [apply Nat.lt_0_succ|]. auto. ring. destruct n. inversion H. auto with arith. apply Nat.le_antisymm; auto. Qed.
imports: Coq(Arith Euclid Compare Lia)