proposition: Theorem Miquel : forall A B C D E F M : PO, A <> C -> A <> F -> B <> E -> B <> C -> alignes A D F -> alignes A E C -> alignes B D E -> alignes B F C -> triangle A E D -> triangle A E M -> triangle B D M -> triangle B F M -> sont_cocycliques A C F M -> sont_cocycliques A E D M -> sont_cocycliques E C B M /\ sont_cocycliques D F B M.
proof: Proof. intros. deroule_triangle A E D. deroule_triangle A E M. deroule_triangle B D M. deroule_triangle B F M. cut (triangle A C M); intros. cut (triangle A C F); intros. cut (triangle B E M); intros. cut (triangle B C M); intros. deroule_triangle A C M. deroule_triangle A C F. deroule_triangle B E M. deroule_triangle B C M. split; [ try assumption | idtac ]. apply cocycliques_ordre_cycle; apply cocycliques_ordre_cycle. apply reciproque_cocyclicite; auto with geo. replace (double_AV (cons_AV (vec E B) (vec E M))) with (double_AV (cons_AV (vec E D) (vec E M))). replace (double_AV (cons_AV (vec E D) (vec E M))) with (double_AV (cons_AV (vec A D) (vec A M))). replace (double_AV (cons_AV (vec A D) (vec A M))) with (double_AV (cons_AV (vec A F) (vec A M))). replace (double_AV (cons_AV (vec C B) (vec C M))) with (double_AV (cons_AV (vec C F) (vec C M))). apply cocyclicite6; auto with geo. apply alignement_et_angles; auto with geo. apply alignement_et_angles; auto with geo. apply cocyclicite6; auto with geo. apply alignement_et_angles; auto with geo. apply cocycliques_ordre_cycle; apply cocycliques_ordre_cycle. apply reciproque_cocyclicite; auto with geo. replace (double_AV (cons_AV (vec D B) (vec D M))) with (double_AV (cons_AV (vec D E) (vec D M))). replace (double_AV (cons_AV (vec D E) (vec D M))) with (double_AV (cons_AV (vec A E) (vec A M))). replace (double_AV (cons_AV (vec A E) (vec A M))) with (double_AV (cons_AV (vec A C) (vec A M))). replace (double_AV (cons_AV (vec F B) (vec F M))) with (double_AV (cons_AV (vec F C) (vec F M))). apply cocyclicite5; auto with geo. apply alignement_et_angles; auto with geo. apply alignement_et_angles; auto with geo. apply cocyclicite5; auto with geo. apply alignement_et_angles; auto with geo. apply alignement_triangle with (3 := H10); auto with geo. apply alignement_triangle with (3 := H9); auto with geo. apply alignement_triangle with (3 := H7); auto with geo. apply alignement_triangle with (3 := H8); auto with geo. Qed.