The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

I guess Qcanon has been done from a copy/paste of another file, so that
"Qcle_lt_or_eq" has probably a typo in its type.

I think that the expected lemma is the following one:

Lemma Qcle_lt_or_eq : forall x y, x<=y -> x<y \/ x=y.

instead of:

Lemma Qcle_lt_or_eq : forall x y, x<=y -> x<y \/ x==y.

There is some lemma I previously reported to be weird (in the sense
that some of its expected hypothesis are always true).

Plus I also have a personal copy of Qabs but using Qc instead of Q.
If the devs are interested in it, I can provide it.

I am also wondering if Q has some interest in comparison to Qc (well
beside the fact that Qc uses Q).