diff options
Diffstat (limited to 'theories/QArith/Qpower.v')
| -rw-r--r-- | theories/QArith/Qpower.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v index 5d494c7c8c..db77567a7c 100644 --- a/theories/QArith/Qpower.v +++ b/theories/QArith/Qpower.v @@ -41,6 +41,7 @@ try destruct (Qmult_integral _ _ H0); auto. Qed. Lemma Qpower_pos_positive : forall p n, 0 <= p -> 0 <= Qpower_positive p n. +Proof. intros p n Hp. induction n; simpl; repeat apply Qmult_le_0_compat;assumption. Qed. |