proposition: Lemma pow2_sqrtk k a : 0 <= a -> pow (sqrtk k a) (pow2 k) = a.
proof: Proof. intros p; induction k; simpl. ring. rewrite <-IHk at 2; clear IHk. replace (pow2 k + (pow2 k + 0))%nat with (2 * pow2 k)%nat by ring. rewrite pow_mult. f_equal. simpl. rewrite <-Rmult_assoc. rewrite sqrt_sqrt. ring. apply sqrtk_pos, p. Qed.
imports: Lia Reals Psatz