proposition: Lemma sont_cocycliques_avec_ordre_permute: forall (A B C D :PO), sont_cocycliques A B C D ->sont_cocycliques A B D C.
proof: Proof. intros A B C D H. deroule_sont_cocycliques . unfold sont_cocycliques . exists x. unfold circonscrit in *. unfold isocele in *. repeat split ;auto. Qed.