proposition: Lemma sont_cocycliques_avec_ordre_cycle: forall (A B C D :PO), sont_cocycliques A B C D ->sont_cocycliques B C D A.
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. rewrite H4 in H2;auto. rewrite H3 in H0;auto. rewrite H4 in H2;auto. Qed.