proposition: Lemma composee_homothetie_translation_exists : forall (k : R) (I A A' : PO), k <> 1 :>R -> k <> 0 :>R -> exists J : PO, (forall B B' B1 : PO, B1 = homothetie k I B :>PO -> B' = translation A A' B1 :>PO -> B' = homothetie k J B :>PO).
proof: Proof. intros. exists (barycentre (cons 1 A') (cons (-1 + (1 + - k)) (barycentre (cons (-1) A) (cons (1 + - k) I)))); intros. apply composee_homothetie_translation with (4 := H2) (3 := H1); auto. Qed.