proposition: Lemma NRoot_cancel : forall x Hx y Hy k Hk, NRoot x k Hx Hk [=] NRoot y k Hy Hk -> x [=] y.
proof: Proof. intros. apply eq_transitive_unfolded with (NRoot x k Hx Hk[^]k). apply eq_symmetric_unfolded; apply NRoot_power. apply eq_transitive_unfolded with (NRoot y k Hy Hk[^]k). 2: apply NRoot_power. apply nexp_wd; algebra. Qed.
imports: CoRN.reals.OddPolyRootIR