proposition: Lemma sqrtk_pow2 k a : 0 <= a -> sqrtk k (pow 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 (pow2 k * 2)%nat by ring. rewrite pow_mult. simpl. rewrite Rmult_1_r, sqrtk_mult, sqrt_square. auto. apply sqrtk_pos. all:apply pow_le; auto. Qed.
imports: Lia Reals Psatz