proposition: Lemma compo_homothetie_I : forall (k k' : R) (I A A' A1 : PO), A1 = homothetie k I A :>PO -> A' = homothetie k' I A1 :>PO -> A' = homothetie (k' * k) I A.
proof: Proof. intros k k' I A A' A1 H H0; try assumption. cut (vec I A' = mult_PP (k' * k) (vec I A)); intros. apply vecteur_homothetie; auto. rewrite <- mult_mult_vec. rewrite <- (homothetie_vecteur (k:=k) (I:=I) (A:=A) (A':=A1)); auto. apply homothetie_vecteur; auto. Qed.