diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-16 12:59:21 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-16 12:59:21 +0000 |
| commit | 3f6db8c182cc45272f1b9988db687bcdd0009ab1 (patch) | |
| tree | b78a392bd35d86e449dc84438eee61d6dd2f2ade /theories/Numbers/NatInt/NZBase.v | |
| parent | 4bf2fe115c9ea22d9e2b4d3bb392de2d4cf23adc (diff) | |
Division in Numbers: more properties proved (still W.I.P.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12591 85f007b7-540e-0410-9357-904b9bb8a0f7
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 2decfafca..1215bfba2 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 ? *) |