proposition: Lemma sqrtk_mult k a b : 0 <= a -> 0 <= b -> sqrtk k (a * b) = sqrtk k a * sqrtk k b.
proof: Proof. intros pa pb; induction k; simpl; auto. rewrite <-sqrt_mult; try apply sqrtk_pos; auto. f_equal; assumption. Qed.
imports: Lia Reals Psatz