proposition: Lemma poly_norm_monic : forall p n H, monic n (poly_norm p n H).
proof: Proof. unfold poly_norm in |- *. unfold monic in |- *. unfold degree in |- *. unfold degree_le in |- *. intros. elim H. intros H0 H1. split. Step_final (([1][/] nth_coeff n p[//]poly_norm_aux p n (pair H0 H1)) [*] nth_coeff n p). intros. astepl (([1][/] nth_coeff n p[//]poly_norm_aux p n (pair H0 H1)) [*] nth_coeff m p). Step_final (([1][/] nth_coeff n p[//]poly_norm_aux p n H) [*][0]). Qed.
imports: CoRN.reals.IVT