proposition: Lemma Qpower_mult_positive : forall a n m, Qpower_positive a (n*m) == Qpower_positive (Qpower_positive a n) m.
proof: Proof. intros a n m. induction n using Pos.peano_ind. - reflexivity. - rewrite Pos.mul_succ_l. rewrite <- Pos.add_1_l. do 2 rewrite Qpower_plus_positive. rewrite IHn. rewrite Qmult_power_positive. reflexivity. Qed.
imports: Zpow_facts Qfield Qreduction