diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-28 23:30:32 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-28 23:30:32 +0000 |
| commit | e97cd3c0cab1eb022b15d65bb33483055ce4cc28 (patch) | |
| tree | e1fb56c8f3d5d83f68d55e6abdbb3486d137f9e2 /theories/ZArith/Znat.v | |
| parent | 00353bc0b970605ae092af594417a51a0cdf903f (diff) | |
Deletion of useless Zdigits_def
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14247 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Znat.v')
| -rw-r--r-- | theories/ZArith/Znat.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index 84262469b..0ae5dea81 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -212,6 +212,16 @@ Proof. case N.compare_spec; intros; subst; trivial. Qed. +Lemma inj_div2 n : Z.of_N (N.div2 n) = Z.div2 (Z.of_N n). +Proof. + destruct n as [|p]; trivial. now destruct p. +Qed. + +Lemma inj_quot2 n : Z.of_N (N.div2 n) = Z.quot2 (Z.of_N n). +Proof. + destruct n as [|p]; trivial. now destruct p. +Qed. + End N2Z. Module Z2N. |