proposition: Lemma existence_orthogonal : forall A B : PO, A <> B :>PO -> ex (fun C : PO => A <> C :>PO /\ orthogonal (vec A B) (vec A C)).
proof: Proof. intros. elim existence_representant_unitaire with (A := A) (B := B); [ intros D H0; try clear existence_representant_unitaire; try exact H0 | auto ]. elim existence_representant_angle with (A := A) (B := D) (C := A) (x := pisurdeux); [ intros C H2; elim H2; intros H3 H4; try clear H2; try exact H4 | auto ]. exists C. split; [ auto with geo | idtac ]. apply pisurdeux_droit. rewrite angles_representants_unitaires; auto with geo. replace (representant_unitaire (vec A C)) with (vec A C); auto with geo. rewrite <- H0; auto. elim def_representant_unitaire2 with (A := A) (B := B) (C := D); auto; intros. elim H2; intros; auto with geo. Qed.