Added theorem Nat.bezout_comm.

[roglo]

In natural numbers, since there are no negatives, Bézout is either ∃ u v, au=bv+1 or ∃ u v, bv=au+1. Two cases are considered in Nat.gcd_bezout. But they are actually the same. The first case is equivalent to the second case (with different pairs (u, v)), providing a≠0 and b≠0. The new theorem Nat.bezout_com transforms one case to the other one.

[herbelin]

That's an interesting property!

Concerning the integration to the library, would the proof have to be reworked a lot so that it can be done in file NGcd.v and thus automatically exported to all implementations of natural numbers? Then Ngcd.gcd_bezout could take benefit of the new commutativity lemma to be a one-line proof.

[roglo]

I first tried to put it in Ngcd.v but there was a problem with eq_dec (not accessible) and especially mul_max_distr_r that I was unable to access too, even with Require Import NMaxMin. I tried to locally copy its code. Failed again: the proof of mul_max_distr_r uses things which uses other things, and so on. Too complicated.

[roglo]

Bon, je l'ai mis dans NGcd.v. J'ai compris qu'il fallait que j'Include NMaxMinProp A. Du coup, mul_max_distr_r passe, mais ça bloque maintenant sur le_max_r Et là, c'est plus compliqué, il va falloir que tu m'aides.

[roglo]

This should be good now.

[herbelin]

Thanks for bullets. That's true that it makes the indentation slowly sliding to the right. Anyway, let's keep it like this. Thanks a lot. I'll merge it tomorrow.

[herbelin]

PS: Please also squash and add a changelog entry as noticed by @Zimmi48 (use dev/tools/make-changelog.sh, give PR number 11127, "10", edit the new file, git add, commit).

[herbelin]

@Zimmi48: do you have further remarks or can I merge?

[Zimmi48]

Well, this PR still contains 6 commits instead of just one or two. I can show Daniel how to squash when I get the chance to see him (not today).

[roglo]

Well, this PR still contains 6 commits instead of just one or two. I can show Daniel how to squash when I get the chance to see him (not today).

I just made it, thanks to @herbelin