proposition: Theorem Nleast_div_ge_monotone : forall n n' p, n <= n' -> n' < p -> Nleast_div_ge n p >= Nleast_div_ge n' p.
proof: Proof. intros. induction H. auto. simpl. destruct (Ndiv_algo (p-S m) p). apply Nat.le_trans with (p-m). apply Nat.sub_le_mono_l. auto. apply Nat.le_trans with (p-n). apply Nat.sub_le_mono_l. auto. apply Nleast_div_ge_ge. apply Nat.le_trans with (S m). auto with arith. auto with arith. apply IHle. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)