proposition: Lemma Copp_Cmult : forall z : C, Copp z = Cmult (Rinj (-1)) z.
proof: Proof. intros. replace (Rinj (-1)) with (Copp oneC). ring. unfold oneC, Rinj in |- *. rewrite Copp_algebrique; auto. RReplace (-0) 0; auto. Qed.