Sect. 3.2.4: stamps lemma

[anton-trunov]

Chances are this is not really an issue. It's just an alternative proof for the stamps lemma:

Lemma addnBAC m n p : n <= m -> n <= p -> (m - n) + p = m + (p - n).
Proof. by move=> le_nm le_np; rewrite addnC !addnBA // addnC. Qed.

Lemma stamps n : 12 <= n -> exists s4 s5, s4 * 4 + s5 * 5 = n.
Proof.
rewrite {2}(divn_eq n 4) => gt11; exists (n %/4 - n %% 4), (n %% 4).
rewrite mulnBl addnBAC -?mulnBr ?muln1 ?leq_mul //.
by apply: (@leq_trans _ (n %% 4) _ (@ltn_pmod n 4 isT) (leq_div2r 4 gt11)).
Qed.

This approach does not use strong induction, hence it cannot be used for the same purposes as the original proof. Feel free to use this solution in any way you find suitable -- I'm also fine with closing this "issue" since I'm putting it here in case the proof can be useful to anyone.

[gares]

Thanks!

I think the fist lemma should be a PR on math-comp, so that others can comment on it and eventually merge it in the library.

The proof is nice, I may turn it into an exercise, thanks for sharing it. I reworked it a little in order to get rid of {2} and the various @, here it is:

Lemma stamps n : 12 <= n -> exists s4 s5, s4 * 4 + s5 * 5 = n.
Proof.
move=> /leq_div2r leq12n; exists (n %/4 - n %% 4), (n %% 4).
rewrite mulnBl addnBAC -?mulnBr ?muln1 ?leq_mul -?divn_eq //.
by rewrite (leq_trans _ (leq12n 4)) // -ltnS ltn_pmod.
Qed.

It is mostly about shuffling proof steps. The only real difference is that I use ltnS to make step that in your proof is purely computational. That was really smart, but maybe a bit too hard for me ;-)

[anton-trunov]

Thank you! I appreciate your words very much. Your version is really nice! And thanks for the exercise :)

I think the fist lemma should be a PR on math-comp, so that others can comment on it and eventually merge it in the library.

All right, I'll make a PR. Thank you for the suggestion.