proposition: Lemma angles_droites_droites_orthogonales : forall A B C D E F G I : PO, A <> B :>PO -> C <> D :>PO -> E <> F :>PO -> G <> I :>PO -> orthogonal (vec A B) (vec E F) -> orthogonal (vec C D) (vec G I) -> cons_AD (droite E F) (droite G I) = cons_AD (droite A B) (droite C D).
proof: Proof. intros. apply AV_vers_AD; auto. apply angles_droites_orthogonales; auto. Qed.