proposition: Lemma l8_22 : forall A B P R X , A <> B -> A <> P -> Per B A P -> Per A B R -> 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. assert (Cong A R P B). apply (per_cong A B P R X); assumption. split. assumption. assert (~ Col B A P). apply per_not_col. auto. assumption. assumption. apply l7_21; Col; Cong. intro; treat_equalities; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR