proposition: Theorem cocyclicite : forall A B C D : PO, triangle A B C -> triangle A B D -> sont_cocycliques A B C D -> double_AV (cons_AV (vec C A) (vec C B)) = double_AV (cons_AV (vec D A) (vec D B)).
proof: Proof. unfold sont_cocycliques in |- *; intros. deroule_triangle A B C. deroule_triangle A B D. elim H1; (clear H1; (intros O; intros)). elim H1; (clear H1; intros). lapply (circonscrit_triangle_non_point (O:=O) (A:=A) (B:=B) (C:=C)); auto; intros. lapply (circonscrit_triangle_non_point (O:=O) (A:=A) (B:=B) (C:=D)); auto; intros. elim H12; (clear H12; intros). elim H13; (clear H13; intros). elim H11; (clear H11; intros). elim H15; (clear H15; intros). lapply (angle_inscrit2 (O:=O) (A:=A) (B:=B) (C:=C)); auto; intros. lapply (angle_inscrit2 (O:=O) (A:=A) (B:=B) (C:=D)); auto; intros. rewrite H18; auto. try exact H1. try exact H10. Qed.