proposition: Lemma a_oneC_translation : a = oneC -> exists A : PO, (forall M : PO, g M = translation O A M).
proof: Proof. intros. elim existence_image_complexe with (z := b); intros A H1; try clear existence_image_complexe; try exact H1. exists A; intros. elim existence_affixe_point with (M := M); intros z H2; try clear existence_affixe_point; try exact H2. elim existence_affixe_point with (M := g M); intros z'; intros; try exact H2. apply (complexe_translation (a:=b) (z:=z) (z':=z') (A:=A) (M:=M) (M':=g M)); auto with geo. rewrite H0; rewrite g_def; rewrite H2; rewrite affixe_transforme; rewrite f_def; rewrite H; ring. Qed.