proposition: Lemma cercle_trivial : forall A B C D O : PO, circonscrit O A B C -> O = milieu A D -> sont_cocycliques A B C D.
proof: Proof. icercle. exists O. split; [ split; [ try assumption | try assumption ] | try assumption ]. split; [ try assumption | auto with geo ]. Qed.