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