proposition: Lemma homothetie_paralleles : forall (k : R) (I A A' B B' C C' D D' : PO), k <> 0 :>R -> A <> B -> C <> D -> paralleles (droite A B) (droite C D) -> A' = homothetie k I A :>PO -> B' = homothetie k I B -> C' = homothetie k I C :>PO -> D' = homothetie k I D :>PO -> paralleles (droite A' B') (droite C' D').
proof: Proof. intros. elim paralleles_vecteur with (A := A) (B := B) (C := C) (D := D); [ intros x H7; try clear paralleles_vecteur | auto | auto | auto ]. apply colineaires_paralleles with x. apply (image_homothetie_distincts (k:=k) (I:=I) (A:=A) (A':=A') (B:=B) (B':=B')); auto. apply (image_homothetie_distincts (k:=k) (I:=I) (A:=C) (A':=C') (B:=D) (B':=D')); auto. rewrite (homothetie_bipoint (k:=k) (I:=I) (A:=A) (B:=B) (A':=A') (B':=B')); auto. rewrite (homothetie_bipoint (k:=k) (I:=I) (A:=C) (B:=D) (A':=C') (B':=D')); auto. rewrite H7; Ringvec. Qed.