proposition: Lemma nonzero_amoins_un : forall a : C, a <> oneC -> Cplus oneC (Copp a) <> zeroC.
proof: Proof. intros. red in |- *; intros; apply H. replace a with (Cplus a zeroC); [ idtac | ring ]. rewrite <- H0; ring. Qed.