proposition: Lemma _X_monic : forall a : R, monic 1 (_X_ [-] _C_ a).
proof: Proof. split. reflexivity. intro m; destruct m. intro H; inversion H. destruct m. intro H; destruct (Nat.lt_irrefl _ H). reflexivity. Qed.
imports: CPoly_Degree CPoly_Euclid RingClass CRingClass