proposition: Lemma poly_norm_apply : forall p n H x, (poly_norm p n H) ! x [=] [0] -> p ! x [=] [0].
proof: Proof. unfold poly_norm in |- *. intros. apply mult_cancel_lft with ([1][/] nth_coeff n p[//]poly_norm_aux p n H). apply div_resp_ap_zero_rev. apply ring_non_triv. astepl ((_C_ ([1][/] nth_coeff n p[//]poly_norm_aux p n H)) ! x[*]p ! x). astepl (_C_ ([1][/] nth_coeff n p[//]poly_norm_aux p n H) [*]p) ! x. Step_final ([0]:R). Qed.
imports: CoRN.reals.IVT