proposition: Lemma Qcpower_pos : forall p n, 0 <= p -> 0 <= p^n.
proof: Proof. induction n; simpl; auto with qarith. - easy. - intros. apply Qcle_trans with (0*(p^n)). + easy. + apply Qcmult_le_compat_r; auto. Qed.
imports: Field QArith Znumtheory Eqdep_dec