proposition: Lemma part_function_NRoot_strext : forall x y Hx Hy, NRoot (Ext2R x Hx) Hn [#] NRoot (Ext2R y Hy) Hn -> x [#] y.
proof: Proof. intros x y Hx Hy H. refine (pfstrx _ _ _ _ _ _ (NRoot_str_ext _ _ _ _ _ _ _ H)). Qed.
imports: CoRN.reals.OddPolyRootIR