proposition: Lemma composee_translation_homothetie : forall (k : R) (A A' B B' B1 I J : PO), k <> 1 -> k <> 0 -> B1 = translation A A' B :>PO -> B' = homothetie k I B1 :>PO -> J = barycentre (cons (- k) A) (cons (k + (1 + - k)) (barycentre (cons k A') (cons (1 + - k) I))) :>PO -> B' = homothetie k J B.
proof: Proof. unfold translation, homothetie in |- *; intros k A A' B B' B1 I J H H0 H1 H2 H30. elim cons_inj with (a := 1) (b := 1) (A := B') (B := barycentre (cons k B) (cons (1 + - k) (barycentre (cons (- k) A) (cons (k + (1 + - k)) (barycentre (cons k A') (cons (1 + - k) I)))))); intros; auto with *. rewrite H4; rewrite H30; auto. rewrite H2. rewrite H1. replace 1 with (k + (1 + - k)) at 1; [ idtac | try ring ]. rewrite <- add_PP_barycentre; try lra. rewrite <- (homogene_barycentre (a:=(- 1)) (b:=2) (k:=k)); try lra. replace k with (k * -1 + k * 2) at 1 by ring. rewrite <- add_PP_barycentre; try lra. rewrite <- (homogene_barycentre (a:=1) (b:=1) (k:=k)); try lra. replace (k * 2) with (k * 1 + k * 1) at 1 by ring. rewrite <- add_PP_barycentre; try lra. replace 1 with (k + (1 + - k)) at 4; try lra. rewrite <- add_PP_barycentre; try lra. replace (1 + - k) with ((- k) + (k + (1 + - k))) at 2; try lra. rewrite <-!add_PP_barycentre; try lra. RingPP. Qed.