proposition: Lemma cocycliques_ordre_permute : forall A B C D : PO, sont_cocycliques A B C D -> sont_cocycliques A C B D.
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; try assumption ]. split; try assumption. Qed.