proposition: Lemma Ndiv_mod_algo_rem2 : forall n m r, n > 0 -> Ndiv_mod_algo n m = r -> r <= m.
proof: Proof. induction m. intros. destruct n; compute in H0; rewrite <- H0; auto with arith. intros. simpl in H0. destruct n. inversion H. destruct (Nat.eqb (S n) (S (Ndiv_mod_algo (S n) m))). rewrite <- H0. auto with arith. destruct r. inversion H0. apply eq_add_S in H0. apply le_n_S. apply IHm. auto. auto. Qed.
imports: Coq(Arith Euclid Compare Lia)