proposition: Theorem Ngreatest_div_le_le : forall n p, n > 0 -> Ngreatest_div_le n p <= n.
proof: Proof. intros. induction n. inversion H. simpl. destruct n. auto. destruct (Ndiv_algo (S (S n)) p). auto. eapply Nat.le_trans. eapply IHn. auto with arith. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)