proposition: Lemma Morley_3: forall (a b c r : R) (A B C P : PO), 0 < a -> 0 < b -> 0 < c -> (a + b) + c = pisurtrois -> A <> B -> A <> C -> B <> C -> B <> P -> rayon_circonscrit A B C r -> image_angle b = cons_AV (vec B C) (vec B P) -> image_angle c = cons_AV (vec C P) (vec C B) -> image_angle (3 * a) = cons_AV (vec A B) (vec A C) -> distance C P = (8 * (r * sin a)) * (sin b * sin (pisurtrois + a)).
proof: Proof. unfold rayon_circonscrit; intros. elim H7; clear H7; [intros O [H13 H12]]. assert (triangle A B C). apply (pisurtrois_triangle_utile (a:=a) (b:=b) (c:=c) (A:=A) (B:=B) (C:=C)); auto. assert (triangle B C P). apply (pisurtrois_triangle_utile2 (a:=a) (b:=b) (c:=c) (B:=B) (C:=C) (P:=P)); auto. deroule_triangle B C P. clear H17 H14 H15. assert (distance C P = (2 * (r * sin (3 * a))) * (sin b / sin (pisurtrois - a))). assert (distance B C = 2 * (r * sin (3 * a))). rewrite (rayon_Sinus (A:=A) (B:=B) (C:=C) (O:=O)); auto. rewrite H12. rewrite <- (egalite_sin_Sin (A:=A) (B:=B) (C:=C) (x:=3 * a)); auto. rewrite Rabs_right; eauto with geo. rewrite <- H14. rewrite <- H2. RReplace (((a + b) + c) - a) (b + c). elim pi_moins_x with ( x := b + c ); [intros]. rewrite <- H17. elim (loi_Sinus (A:=C) (B:=B) (C:=P)); intros; auto with geo. assert (distance C B / Rabs (Sin (cons_AV (vec P C) (vec P B))) = distance P C / Rabs (Sin (cons_AV (vec B P) (vec B C)))). rewrite <- H19; auto. assert (distance P C = (distance C B / Rabs (Sin (cons_AV (vec P C) (vec P B)))) * Rabs (Sin (cons_AV (vec B P) (vec B C)))). rewrite H20. field. auto with geo. rewrite distance_sym. rewrite H21. rewrite distance_sym. assert (image_angle (- b) = cons_AV (vec B P) (vec B C)). apply mes_oppx; auto. assert (image_angle (- c) = cons_AV (vec C B) (vec C P)). apply mes_oppx; auto. rewrite <- (egalite_sin_Sin (A:=B) (B:=P) (C:=C) (x:=- b)); auto. rewrite sin_impaire. rewrite (Rabs_neg (r:=- sin b)). assert (image_angle (pi + (b + c)) = cons_AV (vec P C) (vec P B)). rewrite <- (angle_triangle (A:=C) (B:=B) (C:=P)); auto. rewrite <- H23. rewrite <- H22. rewrite <- add_mes_compatible. rewrite <- mes_opp. rewrite <- add_mes_compatible. RReplace (- (- c + - b)) (b + c); auto. rewrite <- (egalite_sin_Sin (A:=P) (B:=C) (C:=B) (x:=pi + (b + c))); auto. rewrite H17. elim pi_plus_x with ( x := b + c ); intros. rewrite H26. rewrite Rabs_neg. field. assert (- sin (b + c) <> 0). rewrite <- H26. apply (triangle_sin_not_0 (A:=P) (B:=C) (C:=B) (x:=pi + (b + c))); auto with geo. auto with real. assert (sin (b + c) >= 0); eauto with geo. lra. assert (sin b >= 0). apply sin_pos. apply (pisurtrois_utile2 H H1 H0); auto with real. rewrite <- H2; ring. lra. rewrite H14. rewrite sin_3_a_pisurtrois; auto. field. rewrite <- H2. RReplace (((a + b) + c) + - a) (b + c); auto. assert (image_angle (- c) = cons_AV (vec C B) (vec C P)). apply mes_oppx; auto. assert (image_angle (- b) = cons_AV (vec B P) (vec B C)). apply mes_oppx; auto. assert (image_angle (pi + (b + c)) = cons_AV (vec P C) (vec P B)). rewrite <- (angle_triangle (A:=C) (B:=B) (C:=P)); auto. rewrite <- H15. rewrite <- H17. rewrite <- add_mes_compatible. rewrite <- mes_opp. rewrite <- add_mes_compatible. RReplace (- (- c + - b)) (b + c); auto. elim pi_plus_x with ( x := b + c ); intros. assert (- sin (b + c) <> 0). rewrite <- H20. apply (triangle_sin_not_0 (A:=P) (B:=C) (C:=B) (x:=pi + (b + c))); auto with geo. replace (a + b + c - a) with (b + c) by ring. auto with real. Qed.