proposition: Lemma triangle_rectangle_Cos : forall (A B C : PO) (a : R), A <> B -> A <> C -> orthogonal (vec B A) (vec B C) -> distance A B = distance A C * Cos (cons_AV (vec A B) (vec A C)).
proof: Proof. intros. cut (scalaire (vec A B) (vec A C) = distance A B * (distance A C * Cos (cons_AV (vec A B) (vec A C)))); intros. 2: apply produit_scalaire_Cosinus; auto. apply Rmult_eq_reg_l with (distance A B); auto with geo. rewrite <- H2. rewrite (scalaire_avec_projete (A:=A) (B:=B) (C:=C) (H:=B)); auto with geo. Qed.