proposition: Theorem Ngreatest_div_le_monotone : forall n n' p, n <= n' -> Ngreatest_div_le n p <= Ngreatest_div_le n' p.
proof: Proof. intros. induction H. auto. eapply Nat.le_trans. eexact IHle. assert (Ndiv_algo (S m) p=true -> Ngreatest_div_le (S m) p=S m). intros. simpl. destruct m. auto. rewrite H0. auto. assert (Ndiv_algo (S m) p=false -> Ngreatest_div_le (S m) p=Ngreatest_div_le m p). intros. simpl. destruct m. compute. auto. rewrite H1. auto. destruct (Ndiv_algo (S m) p). rewrite H0. destruct m. compute. auto. eapply Nat.le_trans. eapply Ngreatest_div_le_le. auto with arith. auto with arith. auto. rewrite H1. auto. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)