proposition: Lemma cocyclicite5 : forall A B C D : PO, D <> C -> triangle A B C -> triangle A B D -> sont_cocycliques A B C D -> double_AV (cons_AV (vec A B) (vec A D)) = double_AV (cons_AV (vec C B) (vec C D)) :>AV.
proof: Proof. intros. deroule_triangle A B C. deroule_triangle A B D. elim H2. intros O; intros. elim H11; intros. deroule_circonscrit A B D O. deroule_circonscrit A B C O. rewrite (angle_inscrit (O:=O) (A:=A) (B:=B) (C:=D)); auto. rewrite (angle_inscrit (O:=O) (A:=C) (B:=B) (C:=D)); auto. apply circonscrit_permute. apply circonscrit_trans with A; auto. apply circonscrit_ordre_permute; auto. apply circonscrit_ordre_permute; auto. Qed.