proposition: Lemma Cring : @ring_theory C C0 C1 Cadd Cmult Cminus Copp (eq(A:=C)).
proof: Proof. constructor. exact Cadd_0_l. exact Cadd_comm. intros ; rewrite <- Cadd_assoc ; reflexivity. exact Cmult_1_l. exact Cmult_comm. symmetry; apply Cmult_assoc. intros; apply Cmult_add_distr_r. reflexivity. exact Cadd_opp_r. Qed.
imports: Nnat Arith Ring Field Cbase Cpow