proposition: Lemma constant_pos : [0] [<] C.
proof: Proof. unfold C. apply (less_leEq_trans _ _ [1]). apply pos_one. apply lft_leEq_Max. Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots