proposition: Lemma Rpow_mult_distr : forall x y n, (x * y) ^ n = x ^ n * y ^ n.
proof: Proof. intros x y n; induction n; simpl. field. repeat (rewrite Rmult_assoc); apply Rmult_eq_compat_l. rewrite IHn; field. Qed.
imports: Reals Lra Rfunctions