proposition: Lemma compo_homothetie_IJ_non1_exists : forall (k k' : R) (I J : PO), k' * k <> 1 -> exists K : PO, (forall A A' A1 : PO, A1 = homothetie k I A -> A' = homothetie k' J A1 :>PO -> A' = homothetie (k' * k) K A :>PO).
proof: Proof. intros. exists (barycentre (cons (k' * (1 + - k)) I) (cons (1 + - k') J)); intros. apply compo_homothetie_IJ_non1 with (2 := H0) (3 := H1); auto. Qed.