proposition: Lemma Ndiv_mod_algo_rem : forall n m r, n > 0 -> Ndiv_mod_algo n m = r -> r < n.
proof: Proof. induction m. intros. destruct n. inversion H. compute in H0. rewrite <- H0. auto with arith. intros. destruct n. inversion H. simpl in H0. assert (Ndiv_mod_algo (S n) m<(S n)). apply IHm. auto with arith. auto. apply le_le_S_eq in H1. destruct H1. apply le_S_n in H1. apply Nat.lt_succ_r in H1. apply Nat.succ_lt_mono in H1. destruct (Nat.eqb n (Ndiv_mod_algo (S n) m)). rewrite <- H0. auto with arith. rewrite <- H0. apply (proj1 (Nat.succ_lt_mono _ _)). auto. apply eq_add_S in H1. rewrite H1 in H0. rewrite Nat.eqb_refl in H0. rewrite <- H0. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)