proposition: Lemma nrt_pow : forall i (H : [0] [<=] q[^]i[*]c), NRoot H lt0n [=] nrtq[^]i[*]nrtc.
proof: Proof. intros. apply root_unique with n. apply NRoot_nonneg. apply mult_resp_nonneg. apply nexp_resp_nonneg. exact zlt_nrtq. apply less_leEq. exact zlt_nrtc. auto. astepl (q[^]i[*]c). astepr ((nrtq[^]i) [^]n[*]nrtc[^]n). astepr (nrtq[^] (i * n) [*]nrtc[^]n). rewrite Nat.mul_comm. astepr ((nrtq[^]n) [^]i[*]nrtc[^]n). unfold nrtq in |- *. unfold nrtc in |- *. apply bin_op_wd_unfolded. apply un_op_wd_unfolded. algebra. algebra. Qed.
imports: CoRN.fta.KneserLemma CoRN.fta.CPoly_Shift CoRN.fta.CPoly_Contin1 Coq(Lia)