Add Symmetric instance for neq in Equalities

theories/Numbers/NatInt/NZBase.v

@@ -21,12 +21,9 @@ Proof.
 intros; split; symmetry; auto.
 Qed.
 
-(* TODO: how register ~= (which is just a notation) as a Symmetric relation,
-    hence allowing "symmetry" tac ? *)
-
 Theorem neq_sym : forall n m, n ~= m -> m ~= n.
 Proof.
-intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
+intros n m H; symmetry; exact H.
 Qed.
 
 Theorem eq_stepl : forall x y z, x == y -> x == z -> z == y.
@@ -86,4 +83,4 @@ Tactic Notation "nzinduct" ident(n) constr(u) :=
   induction_maker n ltac:(apply (fun A A_wd => central_induction A A_wd u)).
 
 End NZBaseProp.
-
+Print NZBaseProp.

theories/Structures/Equalities.v

@@ -134,12 +134,18 @@ Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E.
  Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
  Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
  Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
+#[global]
+ Instance neq_symmetric : Symmetric (fun x y => ~(E.eq x y)).
+ Proof. intros x y H H'; symmetry in H'; exact (H H'). Qed.
 End BackportEq.
 
 Module UpdateEq (E:Eq)(F:IsEqOrig E) <: IsEq E.
 #[global]
  Instance eq_equiv : Equivalence E.eq.
  Proof. exact (Build_Equivalence _ F.eq_refl F.eq_sym F.eq_trans). Qed.
+#[global]
+ Instance neq_symmetric : Symmetric (fun x y => ~(E.eq x y)).
+ Proof. intros x y H H'; symmetry in H'; exact (H H'). Qed.
 End UpdateEq.
 
 Module Backport_ET (E:EqualityType) <: EqualityTypeBoth