proposition: Lemma reciproque_droite_milieu : forall A B C I J : PO, triangle A B C -> I = milieu A B :>PO -> paralleles (droite B C) (droite I J) -> alignes A C J -> J = milieu A C :>PO.
proof: Proof. intros. apply vecteur_milieu. apply (Thales_concours (k:=/ 2) (A:=A) (B:=B) (C:=C) (I:=I) (J:=J)); auto. cut (2 <> 0); intros. auto with real. discrR. apply milieu_vecteur2; auto. Qed.