proposition: Lemma translation_milieu : forall I J A A' B B' M N : PO, A' = translation I J A :>PO -> B' = translation I J B -> M = milieu A B -> N = milieu A' B' -> N = translation I J M.
proof: Proof. intros I J A A' B B' M N H H0 H1 H2; try assumption. apply rec_translation_vecteur; auto. replace (vec M N) with (add_PP (cons (-1) M) (cons 1 N)); auto. apply mult_PP_regulier with 2; try discrR. repeat rewrite <- distrib_mult_cons. replace (2 * 1) with 2; try ring; auto. rewrite H2. rewrite <- add_PP_milieu. replace (2 * -1) with (-1 * 2); try ring; auto. repeat rewrite <- def_mult_PP. rewrite H1. rewrite <- add_PP_milieu. repeat rewrite <- distrib_mult_cons. replace (-1 * 1) with (-1); try ring; auto. rewrite <- calcul; auto. replace (add_PP (cons (-1) B) (cons 1 B')) with (vec B B'); auto. rewrite <- (translation_vecteur (I:=A) (J:=A') (A:=B) (A':=B')); auto. rewrite (translation_vecteur (I:=I) (J:=J) (A:=A) (A':=A')); auto. Ringvec. apply translation_trans with (1 := H); auto. Qed.