proposition: Lemma perp_col2_bis : forall A B C D P Q, Perp A B C D -> Col C D P -> Col C D Q -> P <> Q -> Perp A B P Q.
proof: Proof. intros A B C D P Q HPerp HCol1 HCol2 HCD. apply perp_sym. apply perp_col2 with C D; Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR