proposition: Lemma l7_15 : forall P Q R P' Q' R' A, Midpoint A P P' -> Midpoint A Q Q' -> Midpoint A R R' -> Bet P Q R -> Bet P' Q' R'.
proof: Proof. intros. spliter. eapply l4_6. apply H2. unfold Cong_3. repeat split. eapply l7_13. apply l7_2. apply H. apply l7_2. assumption. eapply l7_13. apply l7_2. apply H. apply l7_2. assumption. eapply l7_13. apply l7_2. apply H0. apply l7_2. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR