proposition: Lemma Morley_6: forall (a b c r : R) (A B C P Q : PO), 0 < a -> 0 < b -> 0 < c -> (a + b) + c = pisurtrois -> A <> B -> A <> C -> B <> C -> B <> P -> B <> Q -> A <> Q -> rayon_circonscrit A B C r -> image_angle b = cons_AV (vec B Q) (vec B A) -> image_angle b = cons_AV (vec B C) (vec B P) -> image_angle b = cons_AV (vec B P) (vec B Q) -> image_angle c = cons_AV (vec C P) (vec C B) -> image_angle a = cons_AV (vec A B) (vec A Q) -> image_angle (3 * a) = cons_AV (vec A B) (vec A C) -> image_angle (3 * c) = cons_AV (vec C A) (vec C B) -> Rsqr (distance P Q) = (Rsqr 8 * (Rsqr r * (Rsqr (sin a) * Rsqr (sin b)))) * Rsqr (sin c).
proof: Proof. intros. rewrite (Morley_5 (a:=a) (b:=b) (c:=c) (r:=r) (A:=A) (B:=B) (C:=C) (P:=P) (Q:=Q)); auto. rewrite (Al_Kashi_pisurtrois (a:=a) (b:=b) (c:=c)); auto. ring. Qed.