proposition: Lemma translation_isometrie : forall A A' B B' C C' : PO, B' = translation A A' B -> C' = translation A A' C -> distance B' C' = distance B C.
proof: Proof. intros. apply Rsqr_inj; auto with real geo. unfold Rsqr in |- *. repeat rewrite <- carre_scalaire_distance. rewrite <- (translation_bipoint (I:=A) (J:=A') (A:=B) (A':=B') (B:=C) (B':=C')) ; auto. Qed.