proposition: Lemma image_zeroC : image zeroC = O.
proof: Proof. elim existence_image_complexe with (z := zeroC); unfold zeroC in |- *; intros M H1; try exact H1. cut (vec O M = add_PP (mult_PP 0 (vec O I)) (mult_PP 0 (vec O J))); intros; eauto with geo. rewrite <- H1. symmetry in |- *. apply vecteur_nul_conf. rewrite H. Ringvec. Qed.