proposition: Lemma l8_10 : forall A B C A' B' C', Per A B C -> Cong_3 A B C A' B' C' -> Per A' B' C'.
proof: Proof. unfold Per. intros. ex_and H D. prolong C' B' D' B' C'. exists D'. split. unfold Midpoint. split. assumption. Cong. unfold Cong_3, Midpoint in *. spliter. induction (eq_dec_points C B). treat_equalities;Cong. assert(OFSC C B D A C' B' D' A'). unfold OFSC. repeat split. assumption. assumption. Cong. eapply cong_transitivity. apply cong_symmetry. apply H4. eapply cong_transitivity. apply cong_commutativity. apply H6. Cong. Cong. Cong. assert (Cong D A D' A'). eapply five_segment_with_def. apply H8. assumption. eapply cong_transitivity. apply cong_symmetry. apply H5. eapply cong_transitivity. apply H1. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR