proposition: Lemma Qpower_0_le : forall (p : Q) (n : Z), 0 <= p -> 0 <= p^n.
proof: Proof. intros p [|n|n] Hp; simpl; try discriminate; try apply Qinv_le_0_compat; apply Qpower_pos_positive; assumption. Qed.
imports: Zpow_facts Qfield Qreduction