proposition: Lemma deux_milieux_tetraedre : forall A B C D I J K L : PO, tetraedre A B C D -> I = milieu D A -> J = milieu D B -> K = milieu C A -> L = milieu C B -> vec I J = vec K L.
proof: Proof. intros. cut (mult_PP 2 (vec I J) = vec A B); intros. cut (mult_PP 2 (vec K L) = vec A B); intros. apply mult_PP_regulier with 2; auto with real. rewrite H5; auto. apply droite_milieu with C; auto. apply droite_milieu with D; auto. Qed.