proposition: Lemma triangle_rectangle_absolu_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 * Rabs (cos a).
proof: Proof. intros. cut (/ distance A C >= 0); intros; auto with geo. cut (distance A B >= 0); intros; auto with geo. cut (cos a >= 0); intros. rewrite Rabs_right; auto with real. apply triangle_rectangle_cos; auto. replace (cos a) with (distance A B * / distance A C). RReplace 0 (0 * / distance A C). apply Rmult_ge_compat_r; auto. rewrite (triangle_rectangle_cos (A:=A) (B:=B) (C:=C) (a:=a)); intros; auto with geo. field. auto with geo. apply Rinv_le_pos; auto with geo. Qed.