diff options
Diffstat (limited to 'theories/Ints/num/NMake.v')
| -rw-r--r-- | theories/Ints/num/NMake.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v index c857da385..8cb779350 100644 --- a/theories/Ints/num/NMake.v +++ b/theories/Ints/num/NMake.v @@ -5182,6 +5182,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^1) with (2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n; case n; clear n. intros H1; rewrite spec_reduce_2; unfold to_Z. apply (znz_of_pos_correct w2_spec). @@ -5189,6 +5190,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^2) with (2 * 2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n; case n; clear n. intros H1; rewrite spec_reduce_3; unfold to_Z. apply (znz_of_pos_correct w3_spec). @@ -5196,6 +5198,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^3) with (2 * 2 * 2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n; case n; clear n. intros H1; rewrite spec_reduce_4; unfold to_Z. apply (znz_of_pos_correct w4_spec). @@ -5203,6 +5206,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^4) with (2 * 2 * 2 * 2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n; case n; clear n. intros H1; rewrite spec_reduce_5; unfold to_Z. apply (znz_of_pos_correct w5_spec). @@ -5210,6 +5214,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^5) with (2 * 2 * 2 * 2 * 2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n; case n; clear n. intros H1; rewrite spec_reduce_6; unfold to_Z. apply (znz_of_pos_correct w6_spec). @@ -5217,6 +5222,7 @@ Qed. rewrite H1; simpl Z_of_nat; change (2^6) with (2 * 2 * 2 * 2 * 2 * 2). unfold base. apply Zpower_le_monotone; split; auto with zarith. + apply Zeq_le; apply Zmult_comm. intros n. intros H1; rewrite spec_reduce_n; unfold to_Z. simpl minus; rewrite <- minus_n_O. |