proposition: Lemma Qpower_mult : forall a n m, a^(n*m) == (a^n)^m.
proof: Proof. intros a [|n|n] [|m|m]; simpl; try rewrite Qpower_positive_1; try rewrite Qpower_mult_positive; try rewrite Qinv_power_positive; try rewrite Qinv_involutive; try reflexivity. Qed.
imports: Zpow_facts Qfield Qreduction