proposition: Lemma triangle_rectangle_cos : forall (A B C : PO) (a : R), A <> B -> A <> C -> orthogonal (vec B A) (vec B C) -> image_angle a = cons_AV (vec A B) (vec A C) -> distance A B = distance A C * cos a.
proof: Proof. intros. rewrite (triangle_rectangle_Cos (A:=A) (B:=B) (C:=C)); auto. rewrite (egalite_cos_Cos (A:=A) (B:=B) (C:=C) (x:=a)); auto. Qed.