proposition: Theorem inversion_cocyclicite : forall (A B C D I : PO) (k : R), k <> 0 -> I <> A -> I <> C -> C <> D -> triangle A B C -> B = inversion I k A -> D = inversion I k C -> sont_cocycliques A B C D.
proof: Proof. intros. deroule_inversion I A B k. deroule_inversion I C D k. apply egalite_puissance_cocycliques with I; auto. deroule_triangle A B C. apply alignes_ordre_cycle; auto. apply alignes_ordre_cycle; auto. rewrite H10; auto. Qed.