proposition: Lemma cocyclicite2 : 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 B C) (vec B A)) = double_AV (cons_AV (vec D C) (vec D A)) :>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:=B) (B:=C) (C:=A)); auto. rewrite (angle_inscrit (O:=O) (A:=D) (B:=C) (C:=A)); auto. apply circonscrit_permute; apply circonscrit_permute. apply circonscrit_trans with B; auto. apply circonscrit_permute; apply circonscrit_permute; auto. Qed.