OK, I was thinking this was going to be straightforward to prove but (a) I'm strapped for time and (b) Stdlib seemingly has nothing connecting `mod`

and `sub`

for nats except `Nat.mod_eq`

and `Nat.divmod_spec`

. If anyone can pitch in and formulate a general lemma connecting `mod`

and `sub`

, I volunteer to submit to Stdlib as Coq PR (unless I missed something):

```
From Coq Require Import Arith.
Lemma add_sub_mod_0 : forall m n : nat, n <> 0 -> (m + (n - m mod n)) mod n = 0.
Proof.
(* induction not likely to help much? *)
```

Not sure how much it helps, but I have managed to write this (I suppose it can be improved: for one thing I have not been agonizing much with Search and finding a most direct/simplest way):

```
Require Import Coq.Arith.Arith.
Lemma add_sub_mod_0 : forall m n : nat,
n <> 0 -> (m + (n - m mod n)) mod n = 0.
Proof.
intros m n H.
destruct m.
- rewrite Nat.Div0.mod_0_l.
rewrite Nat.sub_0_r.
rewrite Nat.Div0.mod_same.
reflexivity.
- rewrite <- Nat.Div0.add_mod_idemp_l.
rewrite <- (Arith_prebase.le_plus_minus_stt
(S m mod n) n).
+ apply Nat.Div0.mod_same.
+ apply Nat.lt_le_incl.
apply Nat.mod_upper_bound.
apply H.
Qed.
```

thanks, here is a shorter version, I'll see if I can figure out some lemma to extract from this:

```
Lemma add_sub_mod_0 : forall m n : nat, n <> 0 -> (m + (n - m mod n)) mod n = 0.
Proof.
intros m n Hn; destruct m.
- rewrite (Nat.mod_0_l _ Hn).
rewrite Nat.sub_0_r.
apply (Nat.mod_same _ Hn).
- rewrite <- (Nat.add_mod_idemp_l _ _ _ Hn).
rewrite Nat.add_comm, Nat.sub_add.
+ apply (Nat.mod_same _ Hn).
+ apply Nat.lt_le_incl.
apply (Nat.mod_upper_bound _ _ Hn).
Qed.
```

Karl Palmskog has marked this topic as resolved.

Pierre Jouvelot has marked this topic as unresolved.

In fact, the `destruct`

is not required:

```
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Lemma add_sub_mod_0 : forall m n : nat, n <> 0 -> (m + (n - m %% n)) %% n = 0.
Proof.
move=> m n /eqP ne0.
by rewrite -modnDml subnKC ?modnn // ltnW // ltn_mod lt0n.
Qed.
```

@Pierre Jouvelot : but that requires mathcomp, not just Arith/the stdlib...

But you are absolutely right, indeed here it is:

```
Require Import Coq.Arith.Arith.
Lemma add_sub_mod_0 : forall m n : nat,
n <> 0 -> (m + (n - m mod n)) mod n = 0.
Proof.
intros m n Hn.
rewrite <- Nat.Div0.add_mod_idemp_l.
rewrite Nat.add_comm.
rewrite Nat.sub_add.
- apply Nat.Div0.mod_same.
- apply Nat.lt_le_incl.
apply Nat.mod_upper_bound.
apply Hn.
Qed.
```

CC: @Karl Palmskog

Nice, let's see what lemmas and in which form can be transferred from ZArith to Arith. I hope I can help.

Last updated: Jun 13 2024 at 21:01 UTC