proposition: Lemma triangle_rectangle_direct_sinus : forall (A B C : PO) (a : R), A <> B -> A <> C -> B <> C -> image_angle pisurdeux = cons_AV (vec B C) (vec B A) -> image_angle a = cons_AV (vec A B) (vec A C) -> distance C B = distance C A * sin a.
proof: Proof. intros. cut (image_angle (pisurdeux + - a) = cons_AV (vec C A) (vec C B)); intros. rewrite sin_cos_pisurdeux_moins_x. rewrite <- cos_paire. rewrite <- (triangle_rectangle_cos (A:=C) (B:=B) (C:=A) (a:=- (pisurdeux + - a))) ; auto with geo. apply mes_oppx; auto. replace (cons_AV (vec C A) (vec C B)) with (plus (image_angle pi) (opp (plus (cons_AV (vec A B) (vec A C)) (cons_AV (vec B C) (vec B A))))); auto with geo. rewrite opp_plus_plus_opp; auto. rewrite <- H3; rewrite <- H2. repeat rewrite <- mes_opp. repeat rewrite <- add_mes_compatible. replace (pisurdeux + - a) with (pi + (- a + - pisurdeux)); auto. unfold pi in |- *; ring. Qed.