proposition: Lemma triangle_translation_trianglesSD: forall I J A A' B B' C C' : PO, triangle A B C -> A' = translation I J A-> B' = translation I J B-> C' = translation I J C -> trianglesSD A B C A' B' C'.
proof: Proof. intros I J A A' B B' C C' H0 H1 H2 H3. unfold trianglesSD. repeat split;[assumption|idtac| (rewrite (@translation_bipoint I J B B' C C');auto); (rewrite (@translation_bipoint I J B B' A A');auto)| (rewrite (@translation_bipoint I J C C' A A');auto); (rewrite (@translation_bipoint I J C C' B B');auto) ]. unfold triangle in *. intro H4. elim H0. halignes H4 k. assert (A=B). apply distance_refl1. rewrite <-(@ translation_isometrie I J A A' B B');auto. apply distance_refl2;assumption. rewrite H;auto with geo. apply colineaire_alignes with (k:=k);auto. rewrite (@translation_bipoint I J A A' B B');auto. rewrite (@translation_bipoint I J A A' C C');auto. Qed.