proposition: Lemma perp_cong : forall A B P R X, A <> B -> A <> P -> Perp A B P A -> Perp A B R B -> Cong A P B R -> Col A B X -> Bet P X R -> Cong A R P B.
proof: Proof. intros. apply (per_cong A B P R X). assumption. assumption. apply perp_per_1. assumption. eapply perp_per_1. auto. apply perp_left_comm;auto. assumption. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR