proposition: Lemma l8_22_bis : 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 /\ Midpoint X A B /\ Midpoint X P R.
proof: Proof. intros. apply l8_22; auto. apply perp_per_1;auto. apply perp_per_1;Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR