proposition: Lemma l4_2 : forall A B C D A' B' C' D', IFSC A B C D A' B' C' D' -> Cong B D B' D'.
proof: Proof. unfold IFSC. intros. spliter. induction (eq_dec_points A C). treat_equalities;assumption. assert (exists E, Bet A C E /\ C <> E) by apply point_construction_different. ex_and H6 E. prolong A' C' E' C E. assert (Cong E D E' D') by ( apply (five_segment_with_def A C E D A' C' E' D');[ unfold OFSC; repeat split;Cong| assumption]). apply (five_segment_with_def E C B D E' C' B' D'). unfold OFSC. repeat split; try solve [eBetween| Cong ]. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch03_bet GeoCoq.Tarski_dev.Tactics.CongR