proposition: Lemma composee_homothetie_translation : forall (k : R) (A A' B B' B1 I J : PO), k <> 1 -> k <> 0 -> B1 = homothetie k I B :>PO -> B' = translation A A' B1 :>PO -> J = barycentre (cons 1 A') (cons (-1 + (1 + - k)) (barycentre (cons (-1) 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 1 A') (cons (-1 + (1 + - k)) (barycentre (cons (-1) A) (cons (1 + - k) I)))))); intros; auto with *. rewrite H4; rewrite H30; auto. rewrite H2. rewrite H1. pattern 1 at 1 in |- *. replace 1 with (-1 + 2); [ idtac | try ring ]. rewrite <- add_PP_barycentre; try lra. replace 2 with (1 + 1) by ring. rewrite <- add_PP_barycentre; try lra. replace 1 with (k + (1 + - k)) at 2; try ring. rewrite <- add_PP_barycentre; try lra. replace 1 with (k + (1 + - k)) at 3; try ring. rewrite <- add_PP_barycentre; try lra. replace (1 + - k) with (1 + (-1 + (1 + - k))) at 2; try ring. rewrite <-!add_PP_barycentre; try lra. RingPP. Qed.