proposition: Theorem Nprime_greatest_div_le_1 : forall n p, n<p -> Nprime p -> Ngreatest_div_le n p=1.
proof: Proof. induction n. intros. compute. auto. intros. simpl. destruct n. auto. assert(~(Ndiv_algo (S (S n)) p=true)). intro. destruct H0. apply H2 with (S(S n)). split. auto with arith. auto. apply Ndiv_algo_complete. auto with arith. auto. destruct (Ndiv_algo (S (S n)) p). contradiction H1. auto. apply IHn. auto with arith. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)