proposition: Theorem tangente : forall A B O T : PO, A <> B -> O <> A -> O <> B -> A <> T -> isocele O A B -> orthogonal (vec A T) (vec O A) -> double_AV (cons_AV (vec A T) (vec A B)) = cons_AV (vec O A) (vec O B).
proof: Proof. intros A B O T H H0 H1 H2 H3 H4; try assumption. lapply (isocele_angles_base (A:=O) (B:=A) (C:=B)); auto; intros. lapply (orthogonal_angles (A:=A) (B:=T) (C:=O) (D:=A)); auto; intros. lapply (somme_triangle (A:=O) (B:=A) (C:=B)); auto; intros. replace (cons_AV (vec O A) (vec O B)) with (plus (image_angle pi) (opp (plus (cons_AV (vec A B) (vec A O)) (cons_AV (vec B O) (vec B A))))). replace (cons_AV (vec A T) (vec A B)) with (plus (cons_AV (vec A T) (vec O A)) (cons_AV (vec O A) (vec A B))). unfold double_AV in |- *. rewrite <- H5; auto. replace (plus (plus (cons_AV (vec A T) (vec O A)) (cons_AV (vec O A) (vec A B))) (plus (cons_AV (vec A T) (vec O A)) (cons_AV (vec O A) (vec A B)))) with (plus (plus (cons_AV (vec A T) (vec O A)) (cons_AV (vec A T) (vec O A))) (plus (cons_AV (vec O A) (vec A B)) (cons_AV (vec O A) (vec A B)))). replace (plus (cons_AV (vec A T) (vec O A)) (cons_AV (vec A T) (vec O A))) with (double_AV (cons_AV (vec A T) (vec O A))); auto. rewrite H6; auto. rewrite opp_plus_plus_opp; auto. replace (cons_AV (vec O A) (vec A B)) with (plus (cons_AV (vec O A) (vec A O)) (cons_AV (vec A O) (vec A B))); auto. rewrite <- angle_plat; auto. rewrite def_opp; auto. mesure A O A B. replace (pi + (pi + x + (pi + x))) with (pi + (x + x) + (pi + pi)). rewrite add_mes_compatible. replace (pi + pi) with deuxpi; auto. rewrite pi_plus_pi. repeat rewrite <- add_mes_compatible. replace (pi + (x + x) + 0) with (pi + (x + x)); auto. ring. ring. rewrite Chasles; auto. mesure A T O A. mesure O A A B. replace (x + x + (x0 + x0)) with (x + x0 + (x + x0)); auto. ring. rewrite Chasles; auto. rewrite <- H7; auto. rewrite opp_plus_plus_opp; auto. rewrite <- H5; auto. mesure A B A O. mesure O A O B. replace (x0 + (x + x) + (- x + - x)) with x0; auto. ring. Qed.