proposition: Theorem symetrique_orthocentre : forall A B C H H' : PO, triangle A B C -> triangle B C H -> H = orthocentre A B C :>PO -> H' = reflexion B C H :>PO -> sont_cocycliques A B C H'.
proof: Proof. intros. deroule_triangle A B C. deroule_triangle B C H. lapply (orthocentre_double (A:=A) (B:=B) (C:=C) (H:=H)); intros. apply cocycliques_ordre_cycle; apply cocycliques_ordre_cycle; apply cocycliques_ordre_cycle. apply reciproque_cocyclicite; auto with geo. unfold triangle in |- *. apply non_axe_image_non_axe with H; auto. rewrite <- H12; auto. unfold double_AV in |- *. rewrite (reflexion_inverse_angle (A:=B) (B:=C) (M:=H) (M':=H')); auto. rewrite def_opp; auto. auto. Qed.