diff options
Diffstat (limited to 'mathcomp/ssreflect/eqtype.v')
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 75a04ef..e4e0003 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -196,14 +196,14 @@ Proof. exact/eqP/eqP. Qed. Hint Resolve eq_refl eq_sym : core. -Variant eq_xor_neq_sym (T : eqType) (x y : T) : bool -> bool -> Set := - | EqNotNeqSym of x = y : eq_xor_neq_sym x y true true - | NeqNotEqSym of x != y : eq_xor_neq_sym x y false false. +Variant eq_xor_neq (T : eqType) (x y : T) : bool -> bool -> Set := + | EqNotNeq of x = y : eq_xor_neq x y true true + | NeqNotEq of x != y : eq_xor_neq x y false false. -Lemma eqPsym (T : eqType) (x y : T) : eq_xor_neq_sym x y (y == x) (x == y). +Lemma eqVneq (T : eqType) (x y : T) : eq_xor_neq x y (y == x) (x == y). Proof. by rewrite eq_sym; case: eqP=> [|/eqP]; constructor. Qed. -Arguments eqPsym {T x y}. +Arguments eqVneq {T} x y, {T x y}. Section Contrapositives. @@ -379,9 +379,6 @@ Proof. by move->; rewrite eqxx. Qed. Lemma predU1r : b -> (x == y) || b. Proof. by move->; rewrite orbT. Qed. -Lemma eqVneq : {x = y} + {x != y}. -Proof. by case: eqP; [left | right]. Qed. - End EqPred. Arguments predU1P {T x y b}. |