proposition: Lemma Morley_4: forall (a b c r : R) (A B C Q : PO), 0 < a -> 0 < b -> 0 < c -> (a + b) + c = pisurtrois -> A <> B -> A <> C -> B <> C -> A <> Q -> rayon_circonscrit A B C r -> image_angle b = cons_AV (vec B Q) (vec B A) -> image_angle a = cons_AV (vec A B) (vec A Q) -> image_angle (3 * c) = cons_AV (vec C A) (vec C B) -> distance B Q = (8 * (r * sin c)) * (sin a * sin (pisurtrois + c)).
proof: Proof. intros. rewrite <- (Morley_3 (a:=c) (b:=a) (c:=b) (r:=r) (A:=C) (B:=A) (C:=B) (P:=Q)); auto with geo. rewrite <- H2; ring. generalize H7; unfold rayon_circonscrit, circonscrit, isocele; intros. elim H11; [intros O [H13 H14]]. elim H13; [intros H12 H15]. exists O. split; auto. split; auto. rewrite <- H12; auto. rewrite H14; rewrite <- H15; auto. Qed.