proposition: Lemma cocycliques_trivial : forall A B C : PO, triangle A B C -> sont_cocycliques A B C A.
proof: Proof. icercle. elim existence_cercle_circonscrit with (A := A) (B := B) (C := C); [ unfold sont_cocycliques, circonscrit, isocele in |- *; intros O H0; try exact H0 | auto ]. exists O. split; [ try assumption | idtac ]. split; [ idtac | auto ]. elim H0; intros H1 H2; try clear H0; try exact H1. Qed.