proposition: Lemma triangle_rectangle_indirect_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 A B C a H H0 H1 H2 H3; try assumption. elim pisurdeux_plus_x with (x := a); [ intros H5 H6; try clear pisurdeux_plus_x; try rewrite <- H5 ]. rewrite <- (triangle_rectangle_cos (A:=C) (B:=B) (C:=A) (a:=pisurdeux + a)); auto with geo. cut (orthogonal (vec B A) (vec B C)); auto with geo. apply pisurdeux_droit. RReplace pisurdeux (- - pisurdeux). apply mes_oppx; auto with geo. RReplace (pisurdeux + a) (- - (pisurdeux + a)). apply mes_oppx; auto with geo. 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. rewrite <- (plus_angle_zero (image_angle (- (pisurdeux + a)))). rewrite <- pi_plus_pi. repeat rewrite <- add_mes_compatible. replace (- (pisurdeux + a) + deuxpi) with (pi + (- a + - - pisurdeux)); auto. unfold deuxpi, pi in |- *; ring. Qed.