proposition: Theorem Ngreatest_div_le_1 : forall n, Ngreatest_div n>=1.
proof: Proof. intros. destruct n. compute. auto. destruct n. compute. auto. apply Ngreatest_div_greatest. auto with arith. auto. auto with arith. apply Ndiv_1. Qed.
imports: Coq(Arith Euclid Compare Lia)