proposition: Lemma perp2_refl : forall A B P, A <> B -> Perp2 A B A B P.
proof: Proof. intros. induction(col_dec A B P). assert(HH:=not_col_exists A B H). ex_and HH X. assert(HH:=l10_15 A B P X H0 H1). ex_and HH Q. unfold Perp2. exists Q. exists P. split; Perp. Col. assert(HH:=l8_18_existence A B P H0). ex_and HH Q. unfold Perp2. exists P. exists Q. split; Perp. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel