proposition: Lemma homothetie_milieu : forall (k : R) (I A A' B B' M N : PO), k <> 0 -> A' = homothetie k I A :>PO -> B' = homothetie k I B :>PO -> M = milieu A B :>PO -> N = milieu A' B' :>PO -> homothetie k I M = N.
proof: Proof. unfold homothetie, milieu in |- *; intros. rewrite H2; rewrite H3; rewrite H1; rewrite H0. elim cons_inj with (a := 2) (b := 2) (A := barycentre (cons k (barycentre (cons 1 A) (cons 1 B))) (cons (1 + - k) I)) (B := barycentre (cons 1 (barycentre (cons k A) (cons (1 + - k) I))) (cons 1 (barycentre (cons k B) (cons (1 + - k) I)))); (intros; auto); try discrR. rewrite <- (homogene_barycentre (a:=k) (b:=1 + - k) (k:=2)); try lra. replace 2 with (2 * k + 2 * (1 + - k)) at 1 by lra. rewrite <- add_PP_barycentre; auto; try lra. rewrite <- (homogene_barycentre (a:=1) (b:=1) (k:=k)); try lra. replace (2 * k) with (k * 1 + k * 1) by ring. rewrite <- add_PP_barycentre; auto; try lra. replace 2 with (1 + 1) at 2 by ring. rewrite <- add_PP_barycentre; auto; try lra. replace 1 with (k + (1 + - k)) at 4 6 by ring. rewrite <-!add_PP_barycentre; auto; try lra. RingPP. Qed.