proposition: Lemma angles_orthogonal : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> double_AV (cons_AV (vec A B) (vec C D)) = image_angle pi :>AV -> orthogonal (vec A B) (vec C D).
proof: Proof. intros. soit_orthogonal A B E. apply ortho_sym. apply paralleles_orthogonal with (A := A) (B := E); auto with geo. apply droites_paralleles_angle; auto. replace (double_AV (cons_AV (vec A E) (vec C D))) with (plus (double_AV (cons_AV (vec A E) (vec A B))) (double_AV (cons_AV (vec A B) (vec C D)))); auto. cut (double_AV (cons_AV (vec A E) (vec A B)) = image_angle pi); intros. rewrite H1; rewrite H4; rewrite <- add_mes_compatible; rewrite <- pi_plus_pi; (unfold deuxpi in |- *; auto). apply orthogonal_angles; auto with geo. rewrite double_Chasles; auto with geo. Qed.