proposition: Theorem Morley: forall (a b c : R) (A B C P Q T : PO), 0 < a -> 0 < b -> 0 < c -> (a + b) + c = pisurtrois -> A <> B -> A <> C -> B <> C -> B <> P -> B <> Q -> A <> T -> C <> T -> image_angle b = cons_AV (vec B C) (vec B P) -> image_angle b = cons_AV (vec B P) (vec B Q) -> image_angle b = cons_AV (vec B Q) (vec B A) -> image_angle c = cons_AV (vec C P) (vec C B) -> image_angle c = cons_AV (vec C T) (vec C P) -> image_angle a = cons_AV (vec A B) (vec A Q) -> image_angle a = cons_AV (vec A Q) (vec A T) -> image_angle a = cons_AV (vec A T) (vec A C) -> equilateral P Q T.
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. assert (triangle B Q A). apply (pisurtrois_triangle_utile2 (a:=a) (b:=b) (c:=c) (B:=B) (C:=Q) (P:=A)); auto. deroule_triangle B Q A. assert (image_angle (3 * a) = cons_AV (vec A B) (vec A C)). RReplace (3 * a) (a + (a + a)). replace (cons_AV (vec A B) (vec A C)) with (plus (cons_AV (vec A B) (vec A Q)) (cons_AV (vec A Q) (vec A C))). replace (cons_AV (vec A Q) (vec A C)) with (plus (cons_AV (vec A Q) (vec A T)) (cons_AV (vec A T) (vec A C))). rewrite <- H15; rewrite <- H16; rewrite <- H17. rewrite <- add_mes_compatible. rewrite <- add_mes_compatible; auto. apply Chasles; auto. apply Chasles; auto. assert (triangle A B C). apply (pisurtrois_triangle_utile (a:=a) (b:=b) (c:=c) (A:=A) (B:=B) (C:=C)); auto. assert (image_angle (3 * b) = cons_AV (vec B C) (vec B A)). RReplace (3 * b) (b + (b + b)). replace (cons_AV (vec B C) (vec B A)) with (plus (cons_AV (vec B C) (vec B P)) (cons_AV (vec B P) (vec B A))). replace (cons_AV (vec B P) (vec B A)) with (plus (cons_AV (vec B P) (vec B Q)) (cons_AV (vec B Q) (vec B A))). rewrite <- H12; rewrite <- H11; rewrite <- H10. rewrite <- add_mes_compatible. rewrite <- add_mes_compatible; auto. apply Chasles; auto. apply Chasles; auto. assert (image_angle (3 * c) = cons_AV (vec C A) (vec C B)). rewrite <- (angle_triangle (A:=A) (B:=B) (C:=C)); auto. rewrite <- H28. rewrite <- H30. rewrite <- add_mes_compatible. rewrite <- mes_opp. rewrite <- add_mes_compatible. rewrite <- pisurtrois_def. rewrite <- H2. RReplace (3 * ((a + b) + c) + - (3 * a + 3 * b)) (3 * c); auto. assert (image_angle c = cons_AV (vec C A) (vec C T)). RReplace c ((3 * c + - c) + - c). rewrite add_mes_compatible. rewrite add_mes_compatible. rewrite H31. assert (image_angle (- c) = cons_AV (vec C B) (vec C P)). apply mes_oppx; auto. pattern (image_angle (- c)) at 1. rewrite H32. replace (plus (cons_AV (vec C A) (vec C B)) (cons_AV (vec C B) (vec C P))) with (cons_AV (vec C A) (vec C P)). assert (image_angle (- c) = cons_AV (vec C P) (vec C T)). apply mes_oppx; auto. rewrite H33. apply Chasles; auto. symmetry; apply Chasles; auto. elim existence_rayon_circonscrit with ( A := A ) ( B := B ) ( C := C ); [intros O [H33 [r H34]] | auto]. assert (rayon_circonscrit A B C r). unfold rayon_circonscrit. exists O; (split; auto). assert (and (Rsqr (distance P Q) = Rsqr (distance T P)) (Rsqr (distance P Q) = Rsqr (distance Q T))). rewrite (Morley_6 (a:=a) (b:=b) (c:=c) (r:=r) (A:=A) (B:=B) (C:=C) (P:=P) (Q:=Q)); auto. rewrite (Morley_6 (a:=b) (b:=c) (c:=a) (r:=r) (A:=B) (B:=C) (C:=A) (P:=T) (Q:=P)); auto. rewrite (Morley_6 (a:=c) (b:=a) (c:=b) (r:=r) (A:=C) (B:=A) (C:=B) (P:=Q) (Q:=T)); auto. split; ring. rewrite <- H2; ring. exists O. rewrite H34. generalize H33; unfold circonscrit, isocele; intros. elim H36; [intros; (split; auto)]. rewrite <- H38; auto. rewrite <- H37; auto. rewrite <- H2; ring. exists O. rewrite H34. generalize H33; unfold circonscrit, isocele; intros. elim H36; [intros; (split; auto)]. rewrite <- H38; auto. unfold equilateral, isocele. elim H36; [intros]. split. rewrite (distance_sym P T); auto with geo. rewrite (distance_sym Q P); auto with geo. Qed.