proposition: Lemma translation_intersection : forall I J A A' B B' C C' D D' K K' : PO, A <> B -> C <> D -> ~ alignes A B C \/ ~ alignes A B D -> K = pt_intersection (droite A B) (droite C D) -> A' = translation I J A :>PO -> B' = translation I J B -> C' = translation I J C :>PO -> D' = translation I J D :>PO -> K' = translation I J K :>PO -> K' = pt_intersection (droite A' B') (droite C' D').
proof: Proof. intros. elim def_pt_intersection2 with (A := A) (B := B) (C := C) (D := D) (I := K); [ try clear def_pt_intersection2; intros | auto | auto | auto | auto ]. apply def_pt_intersection; auto. apply image_translation_distincts with (2 := H3) (3 := H4); auto. apply image_translation_distincts with (2 := H5) (3 := H6); auto. elim H1; [ intros H10; try clear H1 | intros H10; try clear H1; try exact H10 ]. left. red in |- *; intros; apply H10. apply (translation_alignement (I:=J) (J:=I) (A:=A') (A':=A) (B:=B') (B':=B) (C:=C') (C':=C)); auto with geo. right; red in |- *; intros H1; apply H10. apply (translation_alignement (I:=J) (J:=I) (A:=A') (A':=A) (B:=B') (B':=B) (C:=D') (C':=D)); auto with geo. apply (translation_alignement (I:=I) (J:=J) (A:=A) (A':=A') (B:=B) (B':=B') (C:=K) (C':=K')); auto with geo. apply (translation_alignement (I:=I) (J:=J) (A:=C) (A':=C') (B:=D) (B':=D') (C:=K) (C':=K')); auto with geo. Qed.