proposition: Lemma Qpower_nat_succ: forall (x : Q) (n : nat), Qpower x (Z.of_nat (S n)) = x * Qpower x (Z.of_nat n).
proof: Proof. intros x n. induction n. - cbn. unfold Qmult. cbn. rewrite Z.mul_1_r, Pos.mul_1_r. destruct x as [n d]. reflexivity. - cbn. unfold Qpower_positive. rewrite pow_pos_succ. + reflexivity. + apply Eqsth. + unfold Proper, respectful; intros; subst; reflexivity. + intros a b c. unfold Qmult. destruct a, b, c. cbn. rewrite Z.mul_assoc. rewrite Pos.mul_assoc. reflexivity. Qed.
imports: Reals ZArith QArith Lra Lia