proposition: Lemma angles_complementaires_triangle_rectangle : forall (A B C : PO) (a : R), A <> B -> A <> C -> B <> C -> orthogonal (vec B A) (vec B C) -> image_angle a = cons_AV (vec A B) (vec A C) -> image_angle (pisurdeux + - a) = cons_AV (vec C A) (vec C B) \/ image_angle (- pisurdeux + - a) = cons_AV (vec C A) (vec C B).
proof: Proof. intros. generalize (somme_triangle (A:=A) (B:=B) (C:=C)); intros. replace (cons_AV (vec C A) (vec C B)) with (plus (image_angle pi) (opp (plus (cons_AV (vec A B) (vec A C)) (cons_AV (vec B C) (vec B A))))); auto with geo. rewrite opp_plus_plus_opp; auto. rewrite <- H3. elim orthogonal_pisurdeux_or with (A := B) (B := C) (C := B) (D := A); [ intros H10; try clear orthogonal_pisurdeux_or | intros H10; try clear orthogonal_pisurdeux_or | auto | auto | auto with geo ]. rewrite <- H10. repeat rewrite <- mes_opp. repeat rewrite <- add_mes_compatible. left; try assumption. replace (pisurdeux + - a) with (pi + (- a + - pisurdeux)); auto. unfold pi in |- *; ring. rewrite <- H10. repeat rewrite <- mes_opp. repeat rewrite <- add_mes_compatible. right; try assumption. rewrite <- (plus_angle_zero (image_angle (- pisurdeux + - a))). rewrite <- pi_plus_pi. repeat rewrite <- add_mes_compatible. replace (- pisurdeux + - a + deuxpi) with (pi + (- a + - - pisurdeux)); auto. unfold deuxpi, pi in |- *; ring. Qed.