proposition: Lemma Qpower_minus_positive : forall a (n m:positive), (m < n)%positive -> Qpower_positive a (n-m)%positive == (Qpower_positive a n)/(Qpower_positive a m).
proof: Proof. intros a n m H. destruct (Qeq_dec a 0) as [EQ|NEQ]. - now rewrite EQ, !Qpower_positive_0. - rewrite <- (Qdiv_mult_l (Qpower_positive a (n - m)) (Qpower_positive a m)) by (now apply Qpower_not_0_positive). f_equiv. rewrite <- Qpower_plus_positive. now rewrite Pos.sub_add. Qed.
imports: Zpow_facts Qfield Qreduction