proposition: Lemma Ndiv_mod_l1 : forall n m, n > 0 -> Ndiv_mod_algo n (m + n) = Ndiv_mod_algo n m.
proof: Proof. intros n m. pattern m. apply nat_strong_ind. intros. simpl. induction n. reflexivity. simpl. replace (Ndiv_mod_algo (S n) n) with n. replace (Nat.eqb n n) with true. reflexivity. symmetry. apply Nat.eqb_refl. symmetry. apply Ndiv_mod_l0. auto with arith. intros. induction n. simpl. reflexivity. simpl. replace (Ndiv_mod_algo (S n) (n0+S n)) with (Ndiv_mod_algo (S n) n0); auto. symmetry. apply H. auto with arith. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)