proposition: Lemma homothetie_intersection : forall (k : R) (I A A' B B' C C' D D' K K' : PO), k <> 0 :>R -> A <> B -> C <> D -> ~ alignes A B C \/ ~ alignes A B D -> K = pt_intersection (droite A B) (droite C D) :>PO -> A' = homothetie k I A :>PO -> B' = homothetie k I B -> C' = homothetie k I C :>PO -> D' = homothetie k I D :>PO -> K' = homothetie k I K :>PO -> K' = pt_intersection (droite A' B') (droite C' D') :>PO.
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_homothetie_distincts with (3 := H4) (4 := H5); auto. apply image_homothetie_distincts with (3 := H6) (4 := H7); auto. elim H2; [ intros H11; try clear H2 | intros H11; try clear H2; try exact H11 ]. left. red in |- *; intros; apply H11. apply (homothetie_alignement (k:=/ k) (I:=I) (A:=A') (B:=B') (A':=A) (B':=B) (C:=C') (C':=C)); auto with geo. right; red in |- *; intros H2; apply H11. apply (homothetie_alignement (k:=/ k) (I:=I) (A:=A') (B:=B') (A':=A) (B':=B) (C:=D') (C':=D)); auto with geo. apply (homothetie_alignement (k:=k) (I:=I) (A:=A) (B:=B) (A':=A') (B':=B') (C:=K) (C':=K')); auto with geo. apply (homothetie_alignement (k:=k) (I:=I) (A:=C) (B:=D) (A':=C') (B':=D') (C:=K) (C':=K')); auto with geo. Qed.