make the sentence about == less ambiguous

[gares]

On Thu, 2019-08-01 at 10:45 +0200, Florent Hivert wrote:

  Dear all,

Reading the MathComp book I was surprised reading at the bottom of
page 125
the following sentence:

Whenever we want to state equality between two expressions, if
they live
in an eqType, always use ==.

It seems to suggest that lemmas such as

Lemma subSS n m : m.+1 - n.+1 = m - n.

should be written as

Lemma subSS n m : m.+1 - n.+1 == m - n.

which doesn't look very practical. Is it a mistake or am I missing
something ?