proposition: Theorem Nleast_div_ge_ge : forall n p, n < p -> Nleast_div_ge n p >= p - n.
proof: Proof. induction n. intros. simpl. rewrite Nat.sub_0_r. auto. intros. simpl. destruct (Ndiv_algo (p-S n) p). auto. unfold ge. apply Nat.le_trans with (p-n). apply Nat.sub_le_mono_l. auto. apply IHn. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)