proposition: Lemma cocycliques_ordre_cycle : forall A B C D : PO, sont_cocycliques A B C D -> sont_cocycliques B C D A.
proof: Proof. unfold sont_cocycliques, circonscrit, isocele in |- *; intros. elim H; intros O; intros. elim H0; intros. exists O. elim H1; intros. elim H2; intros; clear H H0 H1 H2. split; [ idtac | split; [ idtac | try assumption ] ]. split; [ try assumption | idtac ]. rewrite <- H5; auto. rewrite <- H5; auto. rewrite <- H3; auto. rewrite <- H5; auto. Qed.