proposition: Theorem tangente_reciproque : forall A B O T 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) -> alignes A T T'.
proof: Proof. intros A B O T T' H H0 H1 H3 H4 H5 H6; try assumption. discrimine A T. apply alignes_angle; auto. unfold double_AV in |- *. replace (cons_AV (vec A T) (vec A T')) with (plus (cons_AV (vec A T) (vec A B)) (cons_AV (vec A B) (vec A T'))); auto. replace (plus (plus (cons_AV (vec A T) (vec A B)) (cons_AV (vec A B) (vec A T'))) (plus (cons_AV (vec A T) (vec A B)) (cons_AV (vec A B) (vec A T')))) with (plus (plus (cons_AV (vec A T) (vec A B)) (cons_AV (vec A T) (vec A B))) (plus (cons_AV (vec A B) (vec A T')) (cons_AV (vec A B) (vec A T')))); auto. replace (plus (cons_AV (vec A B) (vec A T')) (cons_AV (vec A B) (vec A T'))) with (cons_AV (vec O B) (vec O A)); auto. rewrite <- (def_opp (A:=O) (B:=A) (C:=O) (D:=B)); auto. rewrite <- (tangente (A:=A) (B:=B) (O:=O) (T:=T)); auto. unfold double_AV in |- *. rewrite opp_plus_plus_opp; auto. mesure A T A B. replace (x + x + (- x + - x)) with 0; auto. ring. rewrite <- (def_opp (A:=O) (B:=A) (C:=O) (D:=B)); auto. rewrite <- H6. unfold double_AV in |- *. rewrite opp_plus_plus_opp; auto. rewrite def_opp; auto. mesure A T A B. mesure A B A T'. replace (x + x + (x0 + x0)) with (x + x0 + (x + x0)); auto. ring. rewrite Chasles; auto. Qed.