proposition: Lemma Qpower_0_lt (a : Q) (n : Z) : 0 < a -> 0 < a ^ n.
proof: Proof. intros E1. destruct (Qle_lt_or_eq 0 (a ^ n)) as [E2|E2]; try assumption. now apply Qpower_pos, Qlt_le_weak. symmetry in E2. contradict E2. apply Qpower_not_0. intros E3. symmetry in E3. now destruct (Qlt_not_eq 0 a). Qed.
imports: Coq.QArith.QArith Coq.ZArith.ZArith Coq.NArith.NArith Coq.QArith.Qpower Coq.QArith.Qround Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.List