diff options
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Cyclic/Int63/Cyclic63.v | 1 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int63/Int63.v | 3 |
2 files changed, 1 insertions, 3 deletions
diff --git a/theories/Numbers/Cyclic/Int63/Cyclic63.v b/theories/Numbers/Cyclic/Int63/Cyclic63.v index 2a26b6b12a..4bf971668d 100644 --- a/theories/Numbers/Cyclic/Int63/Cyclic63.v +++ b/theories/Numbers/Cyclic/Int63/Cyclic63.v @@ -218,7 +218,6 @@ Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y. apply Zdiv_lt_upper_bound;auto with zarith. apply Z.lt_le_trans with y;auto with zarith. rewrite <- (Zmult_1_r y);apply Zmult_le_compat;auto with zarith. - assert (0 < 2^p);auto with zarith. replace (2^p) with 0. destruct x;change (0<y);auto with zarith. destruct p;trivial;discriminate. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index a3ebe67325..d3fac82d09 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -1428,7 +1428,7 @@ Proof. assert (Hp3: (0 < Φ (WW ih il))). {simpl zn2z_to_Z;apply Z.lt_le_trans with (φ ih * wB)%Z; auto with zarith. apply Zmult_lt_0_compat; auto with zarith. - refine (Z.lt_le_trans _ _ _ _ Hih); auto with zarith. } + } cbv zeta. case_eq (ih <? j)%int63;intros Heq. rewrite -> ltb_spec in Heq. @@ -1465,7 +1465,6 @@ Proof. apply Hrec; rewrite H; clear u H. assert (Hf1: 0 <= Φ (WW ih il) / φ j) by (apply Z_div_pos; auto with zarith). case (Zle_lt_or_eq 1 (φ j)); auto with zarith; intros Hf2. - 2: contradict Heq0; apply Zle_not_lt; rewrite <- Hf2, Zdiv_1_r; auto with zarith. split. replace (φ j + Φ (WW ih il) / φ j)%Z with (1 * 2 + ((φ j - 2) + Φ (WW ih il) / φ j)) by lia. |