proposition: Theorem Nleast_div_ge_least : forall n p q, p > 1 -> q >= 1 -> q < p -> n < p -> q >= p-n -> (q | p) -> Nleast_div_ge n p <= q.
proof: Proof. intros. replace q with (Nleast_div_ge (p-q) p). apply Nleast_div_ge_monotone. unfold ge in H3. destruct (le_dec n p). apply (Nat.add_le_mono_l (p-n) q n) in H3. rewrite Nat.add_comm in H3. rewrite Nat.sub_add in H3. apply (Nat.sub_le_mono_r p (n+q) q) in H3. rewrite Nat.add_sub in H3. auto. auto. apply Nat.le_trans with p. apply Nat.le_sub_l. auto. auto. destruct H1. rewrite Nat.sub_succ_l. rewrite Nat.sub_diag. simpl. rewrite Nat.sub_0_r. apply Ndiv_algo_correct in H4. rewrite H4. auto. auto. auto. rewrite Nat.sub_succ_l. simpl. apply Ndiv_algo_correct in H4. assert(q<=m). auto with arith. apply Nle_plus in H5. destruct H5. rewrite H5. rewrite Nat.add_comm at 2. rewrite Nat.add_sub. rewrite Nat.add_comm. rewrite Nat.add_comm at 1. rewrite Nat.add_sub. rewrite H5 in H4. rewrite Nat.add_comm. rewrite H4. lia. auto with arith. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)