proposition: Lemma compo_homothetie_IJ_1 : 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 -> vec I K = mult_PP (1 + - k') (vec I J) :>PP -> A' = translation I K A.
proof: Proof. intros. cut (vec A A' = mult_PP (1 + - k') (vec I J)); intros. apply rec_translation_vecteur; auto. rewrite H3; rewrite H2; auto. cut (cons 1 A' = add_PP (add_PP (cons (k' * k) A) (cons (k' * (1 + - k)) I)) (cons (1 + - k') J)); intros. unfold vec in |- *. rewrite H3; auto. repeat rewrite add_PP_assoc. replace (k' * (1 + - k)) with (- (k' * k) + k'); try ring; try ring; auto. rewrite H; auto. RingPP. apply compo_homothetie_IJ with A1; auto. Qed.