proposition: Theorem angle_inscrit : forall O A B C : PO, A <> B -> A <> C -> O <> B -> circonscrit O A B C -> double_AV (cons_AV (vec A B) (vec A C)) = cons_AV (vec O B) (vec O C).
proof: Proof. unfold double_AV in |- *; intros O A B C H H0 H2 H4. cut (O <> A); intros. 2: apply circonscrit_distinct3 with (2 := H4); auto. cut (O <> C); intros. 2: apply circonscrit_distinct2 with (2 := H4); auto. generalize (circonscrit_isocele (O:=O) (A:=A) (B:=B) (C:=C)); intros. lapply (circonscrit_isocele (O:=O) (A:=A) (B:=B) (C:=C)); auto; intros. unfold circonscrit in H4. elim H4; clear H4; intros. replace (cons_AV (vec O B) (vec O C)) with (plus (cons_AV (vec O B) (vec O A)) (cons_AV (vec O A) (vec O C))). generalize (somme_triangle (A:=O) (B:=B) (C:=A)); intros. replace (cons_AV (vec O B) (vec O A)) with (plus (image_angle pi) (opp (plus (cons_AV (vec B A) (vec B O)) (cons_AV (vec A O) (vec A B))))). generalize (somme_triangle (A:=O) (B:=A) (C:=C)); intros. replace (cons_AV (vec O A) (vec O C)) with (plus (image_angle pi) (opp (plus (cons_AV (vec A C) (vec A O)) (cons_AV (vec C O) (vec C A))))). replace (opp (plus (cons_AV (vec B A) (vec B O)) (cons_AV (vec A O) (vec A B)))) with (plus (opp (cons_AV (vec B A) (vec B O))) (opp (cons_AV (vec A O) (vec A B)))). replace (opp (plus (cons_AV (vec A C) (vec A O)) (cons_AV (vec C O) (vec C A)))) with (plus (opp (cons_AV (vec A C) (vec A O))) (opp (cons_AV (vec C O) (vec C A)))). replace (cons_AV (vec A B) (vec A C)) with (plus (cons_AV (vec A B) (vec A O)) (cons_AV (vec A O) (vec A C))). rewrite def_opp; auto. rewrite def_opp; auto. rewrite def_opp; auto. rewrite def_opp; auto. generalize (isocele_angles_base (A:=O) (B:=A) (C:=B)); auto; intros. rewrite <- H10; auto. generalize (isocele_angles_base (A:=O) (B:=C) (C:=A)); auto with geo; intros. rewrite <- H11; auto with geo. mesure A B A O. mesure C A C O. replace (pi + (x + x) + (pi + (x0 + x0))) with (pi + pi + (x + x + (x0 + x0))). replace (pi + pi) with deuxpi; auto. symmetry in |- *. rewrite add_mes_compatible; rewrite pi_plus_pi; rewrite <- add_mes_compatible. replace (0 + (x + x + (x0 + x0))) with (x + x0 + (x + x0)); auto. ring. ring. rewrite Chasles; auto. rewrite <- opp_plus_plus_opp; auto. rewrite <- opp_plus_plus_opp; auto. rewrite <- H9; auto. rewrite opp_plus_plus_opp; auto. mesure A C A O. mesure C O C A. mesure O A O C. replace (x1 + (x + x0) + (- x + - x0)) with x1; auto. ring. rewrite <- H8; auto. rewrite opp_plus_plus_opp; auto. mesure B A B O. mesure A O A B. mesure O B O A. replace (x1 + (x + x0) + (- x + - x0)) with x1; auto. ring. rewrite Chasles; auto. Qed.