proposition: Lemma orthogonal_angles : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> orthogonal (vec A B) (vec C D) -> double_AV (cons_AV (vec A B) (vec C D)) = image_angle pi.
proof: Proof. intros. elim existence_representant_unitaire with (A := A) (B := B); [ intros E H2; try clear existence_representant_unitaire; try exact H2 | auto ]. elim existence_representant_angle with (A := A) (B := E) (C := A) (x := pisurdeux); [ intros F H5; elim H5; intros H3 H4; try clear H5; try exact H4 | auto ]. cut (orthogonal (vec A B) (vec A F)); intros. elim (orthogonal_paralleles (A:=A) (B:=B) (C:=F) (E:=C) (F:=D)); auto with geo; intros. cut (x <> 0); intros. rewrite (angles_et_colinearite (A:=A) (B:=B) (C:=C) (D:=D) (E:=A) (F:=B) (G:=A) (I:=F) (k1:=1) (k2:=/ x)); auto with geo. rewrite angles_representants_unitaires; auto with geo. replace (representant_unitaire (vec A F)) with (vec A F); auto with geo. rewrite <- H2; auto. unfold double_AV in |- *; rewrite <- H4. rewrite <- add_mes_compatible; (unfold pi in |- *; auto with geo). Ringvec. rewrite H6. Fieldvec x. red in |- *; intros; apply H0. apply (produit_zero_conf H6); auto. apply pisurdeux_droit. rewrite angles_representants_unitaires; auto with geo. replace (representant_unitaire (vec A F)) with (vec A F); auto with geo. rewrite <- H2; auto. apply carre_scalaire_1_distance; auto. elim def_representant_unitaire2 with (A := A) (B := B) (C := E); auto; intros. elim H4; auto. Qed.