proposition: Lemma Qpower_plus : forall a n m, ~a==0 -> a^(n+m) == a^n*a^m.
proof: Proof. intros a [|n|n] [|m|m] H; simpl; try ring; try rewrite Qpower_plus_positive; try apply Qinv_mult_distr; try reflexivity; rewrite ?Z.pos_sub_spec; case Pos.compare_spec; intros H0; simpl; subst; try rewrite Qpower_minus_positive; try (field; try split; apply Qpower_not_0_positive); assumption. Qed.
imports: Zpow_facts Qfield Qreduction