proposition: Lemma projete_absolu_sin : forall (A B C H : PO) (a : R), triangle A B C -> H = projete_orthogonal A B C -> image_angle a = cons_AV (vec A B) (vec A C) -> distance C H = distance C A * Rabs (sin a).
proof: Proof. intros. deroule_triangle A B C. elim def_projete_orthogonal2 with (A := A) (B := B) (C := C) (H := H); [ intros; auto | auto | auto ]. halignes H7 k. cut (orthogonal (vec H A) (vec H C)); intros; auto with geo. elim Rtotal_order with (r1 := k) (r2 := 0); [ intros H11; try clear total_order | intros H11; elim H11; [ intros H12; try clear H11 total_order | intros H12; try clear H11 total_order; try exact H12 ] ]. replace (Rabs (sin a)) with (Rabs (sin (a + pi))). apply triangle_rectangle_absolu_sinus; auto. apply distinct_produit_vecteur with (3 := H9); auto with real. red in |- *; intros; apply H3. rewrite <- H12; auto with geo. rewrite H9. rewrite angle_produit_negatif_l; auto. rewrite add_mes_compatible; rewrite <- H2; auto. RReplace (a + pi) (pi + a). elim pi_plus_x with (x := a); [ intros H12 H13; try clear pi_plus_x; rewrite H13 ]. rewrite Rabs_Ropp; auto. cut (A = H); intros. rewrite <- H13 in H8; auto. elim droit_direct_ou_indirect with (A := A) (B := B) (C := C); [ intros H14; try clear droit_direct_ou_indirect | intros H14; try clear droit_direct_ou_indirect; try exact H14 | auto | auto | auto ]. replace (sin a) with (sin pisurdeux). rewrite sin_pisurdeux; rewrite Rabs_R1; ring_simplify. rewrite <- H13; auto. apply sin_deux_mes. rewrite H14; auto. replace (sin a) with (sin (- pisurdeux)). rewrite sin_impaire; rewrite sin_pisurdeux. rewrite Rabs_Ropp; rewrite Rabs_R1; ring_simplify. rewrite <- H13; auto. apply sin_deux_mes. rewrite H14; auto. apply produit_zero_conf with (1 := H9); auto. apply triangle_rectangle_absolu_sinus; auto. apply distinct_produit_vecteur with (3 := H9); auto with real. red in |- *; intros; apply H3. rewrite <- H13; auto with geo. rewrite H9; auto. rewrite angle_produit_positif_l; auto. replace (vec H A) with (mult_PP (- k) (vec A B)). Simplortho. VReplace (vec H A) (mult_PP (-1) (vec A H)). rewrite H9; Ringvec. Qed.