I need to prove the following involving `N.div_eucl`

:

```
Lemma xxx (b q r : N) : (r < b)%N → N.div_eucl (b * q + r)%N b = (q, r).
```

This seems to me like the most trivial imaginable property about that function, but I cannot seem to be able to prove it using existing lemmas. Is it just that there are not enough lemmas in the standard library, or am I missing something obvious?

doesn't look like there are lemmas about N.div_eucl other than N.div_eucl_spec which isn't strong enough AFAICT

There are more results on the projections:

```
Definition div a b := fst (div_eucl a b).
Definition modulo a b := snd (div_eucl a b).
```

This leads to:

```
From Coq Require Import NArith.
Open Scope N.
Lemma xxx (b q r : N) : (r < b) -> N.div_eucl (b * q + r) b = (q, r).
Proof.
intro Hr.
rewrite (surjective_pairing (N.div_eucl (b * q + r) b)). f_equal.
- symmetry. apply (N.div_unique (b * q + r) _ _ _ Hr). reflexivity.
- symmetry. apply (N.mod_unique (b * q + r) _ q _ Hr). reflexivity.
Qed.
```

I'd consider adding some `N.div_eucl_eq`

lemma to help discovery, _and_ `xxx`

itself

```
Lemma div_eucl_eq a b :
N.div_eucl a b = (N.div a b, N.modulo a b).
Proof. rewrite /N.div /N.modulo. by destruct N.div_eucl. Qed.
```

I believe `N.div_eucl_eq`

worthwhile even if I already happened to know `N.div`

had more results (I'd seen them in the past).

(I'm afraid I won't get to send a PR myself so I won't judge others)

It is also possible to go through `N.div_eucl_spec`

:

```
From Coq Require Import NArith.
Open Scope N.
Lemma xxx (b q r : N) : r < b -> N.div_eucl (b * q + r) b = (q, r).
Proof.
intro Hr.
assert (Hspec := N.div_eucl_spec (b * q + r) b).
destruct (N.div_eucl (b * q + r) b) as (q', r') eqn:Hdiv_eucl.
apply N.div_mod_unique in Hspec as [-> ->]; [ reflexivity | assumption | ].
change r' with (snd (q', r')). rewrite <- Hdiv_eucl. apply N.mod_lt.
intros ->. exact (N.nlt_0_r _ Hr).
Qed.
```

Last updated: Jun 22 2024 at 16:02 UTC