proposition: Theorem angle_inscrit2 : forall O A B C : PO, A <> C -> B <> C -> O <> B -> circonscrit O A B C -> double_AV (cons_AV (vec C A) (vec C B)) = cons_AV (vec O A) (vec O B).
proof: Proof. intros O A B C H H0 H1 H2; try assumption. cut (O <> A); intros. 2: apply circonscrit_distinct3 with (2 := H2); auto. apply angle_inscrit; auto. hcercle H2. rewrite <- H6; auto. Qed.