proposition: Lemma rec_complexe_translation : forall (a z z' : C) (A M M' : PO), z = affixe M -> z' = affixe M' -> a = affixe A -> M' = translation O A M :>PO -> z' = Cplus z a.
proof: Proof. intros. cut (Cplus z' (Copp z) = a); intros. rewrite <- H3; ring. apply (egalite_vecteur_image (z:=Cplus z' (Copp z)) (z':=a) (A:=M) (B:=M') (A':=O) (B':=A)); auto with geo. symmetry in |- *; apply translation_vecteur; auto. Qed.