Library gaia_hydras.GPrelude
Learning ssreflect:
From
mathcomp
Require
Import
all_ssreflect
zify
.
Lemma
diffP
{
T
:
eqType
}(
i
j
:
T
):
reflect
(
i
≠
j
) (
i
!=
j
).