proposition: Lemma translation_analytique : forall A M M' : PO, M' = translation O A M :>PO -> abscisse M' = abscisse M + abscisse A /\ ordonnee M' = ordonnee M + ordonnee A.
proof: Proof. intros. paffixe M z. paffixe A a. paffixe M' z'. assert (z' = Cplus z a). apply rec_complexe_translation with (4 := H); auto. generalize H0 H1 H2. repeat rewrite <- coordonnees_affixe; intros. apply unicite_parties_relles_imaginaires with z'; auto. rewrite H3; rewrite H4; rewrite H5; rewrite Cplus_algebrique; auto. Qed.