proposition: Lemma intersection_homothetie : 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' = pt_intersection (droite A' B') (droite C' D') :>PO -> K' = homothetie k I K :>PO.
proof: Proof. intros. elim existence_homothetique with (k := k) (I := I) (A := K); intros L H13. rewrite <- H13; rewrite H8; symmetry in |- *. apply (homothetie_intersection (k:=k) (I:=I) (A:=A) (A':=A') (B:=B) (B':=B') (C:=C) (C':=C') (D:=D) (D':=D') (K:=K) (K':=L)); auto. Qed.