proposition: Lemma triangle_rectangle_absolu_sinus : forall (A B C : PO) (a : R), A <> B -> A <> C -> B <> C -> orthogonal (vec B A) (vec B C) -> image_angle a = cons_AV (vec A B) (vec A C) -> distance C B = distance C A * Rabs (sin a).
proof: Proof. intros. cut (/ distance C A >= 0); intros; auto with geo. 2: apply Rinv_le_pos; auto with geo. cut (distance C B >= 0); intros; auto with geo. elim orthogonal_pisurdeux_or with (A := B) (B := C) (C := B) (D := A); [ intros H10; try clear orthogonal_pisurdeux_or | intros H10; try clear orthogonal_pisurdeux_or | auto | auto | auto with geo ]. cut (sin a >= 0); intros. rewrite Rabs_right; auto with real. apply triangle_rectangle_direct_sinus; auto. replace (sin a) with (distance C B * / distance C A). RReplace 0 (0 * / distance C A). apply Rmult_ge_compat_r; auto with geo. rewrite (triangle_rectangle_direct_sinus (A:=A) (B:=B) (C:=C) (a:=a)); intros; auto with geo. field. auto with geo. cut (- sin a >= 0); intros. elim H6; clear H6; intros. rewrite Rabs_left; auto with real. apply triangle_rectangle_indirect_sinus; auto. lra. rewrite Rabs_right; auto with real. replace (sin a) with (- sin a). apply triangle_rectangle_indirect_sinus; auto. rewrite H6. RReplace (sin a) (- - sin a). rewrite H6; ring. RReplace (sin a) (- - sin a). rewrite H6; auto with real. replace (- sin a) with (distance C B * / distance C A). RReplace 0 (0 * / distance C A). apply Rmult_ge_compat_r; auto. rewrite (triangle_rectangle_indirect_sinus (A:=A) (B:=B) (C:=C) (a:=a)); intros; auto with geo. field. auto with geo. Qed.