wip: comments by Arthur

[gares]

New plan:

• discuss strong induction in 3.7, the HO P argument is so powerful to prove it you case use it via elim/strong_ind
• keep or not the stamp example in ch4, but not use ubnP
• in ch 5.3, after the explanation of families with indexes, mention ubnP and eventually use it to prove ltn_ind plus rework the proof of gcd using ubnP