proposition: Lemma compo_homothetie_IJ_non1 : forall (k k' : R) (I J A A' A1 K : PO), k' * k <> 1 -> A1 = homothetie k I A :>PO -> A' = homothetie k' J A1 :>PO -> K = barycentre (cons (k' * (1 + - k)) I) (cons (1 + - k') J) :>PO -> A' = homothetie (k' * k) K A.
proof: Proof. intros; unfold homothetie in |- *. cut (A' = barycentre (cons (k' * k) A) (cons (1 + - (k' * k)) K)); intros. rewrite H3; auto. elim cons_inj with (a := 1) (b := k' * k + (1 + - (k' * k))) (A := A') (B := barycentre (cons (k' * k) A) (cons (1 + - (k' * k)) K)); intros; auto with *. rewrite <- add_PP_barycentre; auto with real. rewrite H2. RReplace (1 + - (k' * k)) (k' * (1 + - k) + (1 + - k')). rewrite <- add_PP_barycentre; auto with real. rewrite add_PP_assoc. apply compo_homothetie_IJ with A1; auto. RReplace (k' * (1 + - k) + (1 + - k')) (1 + - (k' * k)). auto with real. RReplace (k' * k + (1 + - (k' * k))) 1. auto with real. Qed.