proposition: Lemma Morley_2: 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 B P = (8 * (r * sin a)) * (sin c * sin (pisurtrois + a)).
proof: Proof. intros. 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 H13 H12 H15. rewrite (Morley_1 (a:=a) (b:=b) (c:=c) (r:=r) (A:=A) (B:=B) (C:=C) (P:=P)); auto. 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 <- H13. rewrite <- H12. 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 <- H17. 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.