proposition: Theorem mediane : forall A B C I : PO, I = milieu B C -> R4 * Rsqr (distance A I) = R2 * (Rsqr (distance A B) + Rsqr (distance A C)) - Rsqr (distance B C) :>R.
proof: Proof. unfold R2, R4 in |- *; intros. rewrite (longueur_mediane A (B:=B) (C:=C) (I:=I)); auto. rewrite (demi_longueur (A:=B) (B:=C) (I:=I)); unfold R2, R4 in |- *; auto. rewrite (distance_sym B I); auto. ring. Qed.