proposition: Lemma complexe_translation : forall (a z z' : C) (A M M' : PO), z = affixe M -> z' = affixe M' -> a = affixe A -> z' = Cplus z a -> M' = translation O A M :>PO.
proof: Proof. intros. apply rec_translation_vecteur. apply (egalite_affixe_vecteur (z:=a) (z':=Cplus z' (Copp z)) (A:=O) (B:=A) (A':=M) (B':=M')); auto with geo. rewrite H2. ring. Qed.