proposition: Lemma Ndiv_mod_l0 : forall n m, m < n -> Ndiv_mod_algo n m = m.
proof: Proof. induction m. intros. destruct n. inversion H. compute. trivial. intros. destruct n. inversion H. simpl. replace (Ndiv_mod_algo (S n) m) with m. replace (Nat.eqb n m) with false. reflexivity. apply eq_nat_correct. intro. rewrite H0 in H. apply Nat.lt_irrefl in H. contradiction. symmetry. apply IHm. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)