Open gares opened 5 years ago
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 ?
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 ?
On Thu, 2019-08-01 at 10:45 +0200, Florent Hivert wrote: