proposition: Lemma triangle_medianes_triangle : forall A B C I J : PO, triangle A B C -> I = milieu B C :>PO -> J = milieu A B :>PO -> ~ alignes A I J.
proof: Proof. intros. deroule_triangle A B C. red in |- *; intros; apply H2. cut (A <> J); intros. halignes H6 k. cut (k <> 0); intros. apply colineaire_alignes with ((1 + - k) * / k). replace (vec A C) with (mult_PP 2 (vec J I)). replace (vec A B) with (mult_PP 2 (vec A J)). VReplace (vec J I) (add_PP (vec A I) (mult_PP (-1) (vec A J))). rewrite H8. Fieldvec k. rewrite (milieu_vecteur_double (A:=A) (B:=B) (M:=J)); auto with geo. rewrite (droite_milieu (A:=B) (B:=A) (C:=C) (I:=J) (J:=I)); auto with geo. apply distinct_col_nonzero with (2 := H8); auto. rewrite H1; apply milieu_distinct; auto. Qed.