proposition: Theorem droite_Simson : forall A B C M P Q R : PO, triangle A B C -> triangle B C M -> triangle A B M -> triangle A C M -> P = projete_orthogonal B C M -> Q = projete_orthogonal A C M -> R = projete_orthogonal A B M -> (sont_cocycliques A B C M <-> alignes P Q R).
proof: Proof. unfold iff in |- *; intros A B C M P Q R H H0 H1 H2 H3 H4 H5. lapply (projete_ortho_cote (A:=A) (B:=B) (C:=C) (M:=M) (P:=P) (Q:=Q) (R:=R)); auto; intros. deroule_triangle A B C. deroule_triangle B C M. cut (M <> P); intros. elim (def_projete_orthogonal2 (A:=B) (B:=C) (C:=M) (H:=P)); auto; intros. elim (def_projete_orthogonal2 (A:=A) (B:=C) (C:=M) (H:=Q)); auto; intros. elim (def_projete_orthogonal2 (A:=A) (B:=B) (C:=M) (H:=R)); auto; intros. cut (P <> R); intros. cut (P <> Q); intros. split; intros. apply alignes_angle; auto. rewrite H6; auto. cut (double_AV (cons_AV (vec C A) (vec C M)) = double_AV (cons_AV (vec B A) (vec B M))); intros. rewrite H25; auto. rewrite double_Chasles; auto. unfold double_AV in |- *. rewrite Chasles; auto. rewrite <- angle_nul; auto. lapply (cocyclicite3 (A:=A) (B:=B) (C:=C) (D:=M)); auto; intros. rewrite <- def_opp; auto. rewrite <- (def_opp (A:=B) (B:=M) (C:=B) (D:=A)); auto. rewrite double_opp; auto. rewrite double_opp; auto. rewrite H25; auto. lapply (angle_alignes (A:=P) (B:=Q) (C:=R)); auto; intros. cut (sont_cocycliques A M C B); intros. generalize H26; unfold sont_cocycliques, circonscrit, isocele in |- *; intros. elim H27; intros. elim H28; intros. elim H30; intros. elim H29; intros. exists x; auto. apply reciproque_cocyclicite; auto with geo. replace (double_AV (cons_AV (vec C A) (vec C M))) with (plus (double_AV (cons_AV (vec P Q) (vec P R))) (opp (double_AV (cons_AV (vec B M) (vec B A))))). replace (opp (double_AV (cons_AV (vec B M) (vec B A)))) with (double_AV (cons_AV (vec B A) (vec B M))). rewrite H25; auto. rewrite zero_plus_double; auto. rewrite <- double_opp; auto. rewrite def_opp; auto. rewrite H6; auto. replace (opp (double_AV (cons_AV (vec B M) (vec B A)))) with (double_AV (cons_AV (vec B A) (vec B M))). replace (plus (plus (double_AV (cons_AV (vec C A) (vec C M))) (double_AV (cons_AV (vec B M) (vec B A)))) (double_AV (cons_AV (vec B A) (vec B M)))) with (plus (double_AV (cons_AV (vec C A) (vec C M))) (plus (double_AV (cons_AV (vec B M) (vec B A))) (double_AV (cons_AV (vec B A) (vec B M))))). rewrite double_Chasles; auto. rewrite <- angle_nul; auto. rewrite (angle_nul (A:=C) (B:=M)); auto. rewrite double_Chasles; auto. unfold double_AV in |- *. mesure C A C M. mesure B M B A. mesure B A B M. replace (x + x + (x0 + x0 + (x1 + x1))) with (x + x + (x0 + x0) + (x1 + x1)); auto. ring. rewrite <- double_opp; auto. rewrite def_opp; auto. apply non_alignes_distincts2 with M. deroule_triangle A C M. apply (triangle_ortho_cote (A:=A) (B:=B) (C:=C) (M:=M) (P:=P) (Q:=Q)); auto. apply non_alignes_distincts2 with M. deroule_triangle A B M. apply (triangle_ortho_cote2 (A:=A) (B:=B) (C:=C) (M:=M) (P:=P) (Q:=R)); auto. apply projete_non_axe with (2 := H3); auto. Qed.