diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZBase.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZBase.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 2decfafca1..1215bfba2e 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -17,6 +17,11 @@ Local Open Scope NumScope. Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *) +Lemma eq_sym_iff : forall x y, x==y <-> y==x. +Proof. +intros; split; symmetry; auto. +Qed. + (* TODO: how register ~= (which is just a notation) as a Symmetric relation, hence allowing "symmetry" tac ? *) |