proposition: Lemma included_FNRoot : included S P -> (forall x, S x -> forall Hx, [0][<=]F x Hx) -> included S (Dom FNRoot).
proof: Proof. intros H H0. simpl in |- *. unfold extend in |- *. split. apply H; assumption. intros; apply H0; assumption. Qed.
imports: CoRN.reals.OddPolyRootIR