proposition: Lemma perp2_left_comm : forall A B C D P, Perp2 A B C D P -> Perp2 B A C D P.
proof: Proof. unfold Perp2. intros. ex_and H X. ex_and H0 Y. exists X. exists Y. repeat split; Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel