proposition: Lemma compo_homothetie_IJ : forall (k k' : R) (I J A A' A1 : PO), A1 = homothetie k I A :>PO -> A' = homothetie k' J A1 -> cons 1 A' = add_PP (add_PP (cons (k' * k) A) (cons (k' * (1 + - k)) I)) (cons (1 + - k') J) :>PP.
proof: Proof. unfold vec, homothetie in |- *; intros. rewrite H0; rewrite H. rewrite (distrib_mult_cons k (1 + - k) k' A I). rewrite add_PP_barycentre; try discrR. replace (k + (1 + - k)) with 1; try ring; auto. rewrite def_mult_PP. replace (k' * 1) with k'; try ring; auto. rewrite add_PP_barycentre; try discrR. replace (k' + (1 + - k')) with 1; try ring; auto. replace (k' + (1 + - k')) with 1; try ring; try discrR. replace (k + (1 + - k)) with 1; try ring; try discrR. Qed.