proposition: Lemma compo_homothetie_IJ_1_exists : forall (k : R) (I J : PO), k <> 0 -> exists K : PO, (forall A A' A1 : PO, A1 = homothetie k I A -> A' = homothetie (/ k) J A1 :>PO -> A' = translation I K A).
proof: Proof. intros. elim existence_representant_mult_vecteur with (A := I) (B := I) (C := J) (k := 1 + - / k); intros K H3; try clear existence_representant_mult_vecteur. exists K; intros. apply compo_homothetie_IJ_1 with (2 := H0) (3 := H1); auto with *. Qed.