diff options
| author | letouzey | 2011-05-05 15:12:59 +0000 |
|---|---|---|
| committer | letouzey | 2011-05-05 15:12:59 +0000 |
| commit | d2bd5d87d23d443f6e41496bdfe5f8e82d675634 (patch) | |
| tree | d9cb49b25b4e49ccda4dd424ef2595f53d9e61c0 /theories/ZArith/Zpow_facts.v | |
| parent | f1c9bb9d37e3bcefb5838c57e7ae45923d99c4ff (diff) | |
Modularization of BinInt, related fixes in the stdlib
All the functions about Z is now in a separated file BinIntDef,
which is Included in BinInt.Z. This BinInt.Z directly
implements ZAxiomsSig, and instantiates derived properties ZProp.
Note that we refer to Z instead of t inside BinInt.Z,
otherwise ring breaks later on @eq Z.t
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14106 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zpow_facts.v')
| -rw-r--r-- | theories/ZArith/Zpow_facts.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index 7c603c14d2..d9c5f995b1 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -181,16 +181,16 @@ Theorem Zpower_le_monotone2: forall a b c, 0 < a -> b <= c -> a^b <= a^c. Proof. intros a b c H H2. - destruct (Z_le_gt_dec 0 b). + destruct (Z_le_gt_dec 0 b) as [Hb|Hb]. apply Zpower_le_monotone; auto. replace (a^b) with 0. - destruct (Z_le_gt_dec 0 c). - destruct (Zle_lt_or_eq _ _ z0). + destruct (Z_le_gt_dec 0 c) as [Hc|Hc]. + destruct (Zle_lt_or_eq _ _ Hc) as [Hc'|Hc']. apply Zlt_le_weak;apply Zpower_gt_0;trivial. - rewrite <- H0;simpl;auto with zarith. + rewrite <- Hc';simpl;auto with zarith. replace (a^c) with 0. auto with zarith. - destruct c;trivial;unfold Zgt in z0;discriminate z0. - destruct b;trivial;unfold Zgt in z;discriminate z. + destruct c;trivial;unfold Zgt in Hc;discriminate Hc. + destruct b;trivial;unfold Zgt in Hb;discriminate Hb. Qed. Theorem Zmult_power: forall p q r, 0 <= r -> @@ -225,10 +225,10 @@ Proof. apply Zpower_le_monotone;auto with zarith. apply Zpower_le_monotone3;auto with zarith. assert (c > 0). - destruct (Z_le_gt_dec 0 c);trivial. - destruct (Zle_lt_or_eq _ _ z0);auto with zarith. + destruct (Z_le_gt_dec 0 c) as [Hc|Hc];trivial. + destruct (Zle_lt_or_eq _ _ Hc);auto with zarith. rewrite <- H3 in H1;simpl in H1; exfalso;omega. - destruct c;try discriminate z0. simpl in H1. exfalso;omega. + destruct c;try discriminate Hc. simpl in H1. exfalso;omega. assert (H4 := Zpower_lt_monotone a c b H). exfalso;omega. Qed. |