proposition: Lemma l4_16 : forall A B C D A' B' C' D', FSC A B C D A' B' C' D' -> A<>B -> Cong C D C' D'.
proof: Proof. unfold FSC. unfold Col. intros. decompose [or and] H; clear H. assert (Bet A' B' C') by (eapply l4_6;eauto). unfold Cong_3 in *; spliter. assert(OFSC A B C D A' B' C' D') by (unfold OFSC;repeat split; assumption). eapply five_segment_with_def; eauto. assert(Bet B' C' A') by (apply (l4_6 B C A B' C' A'); Cong;auto with cong3). apply (l4_2 B C A D B' C' A' D'). unfold IFSC; unfold Cong_3 in *; spliter; repeat split;Between;Cong. assert (Bet C' A' B') by (eapply (l4_6 C A B C' A' B'); auto with cong3). eapply (five_segment_with_def B A C D B' A'); unfold OFSC; unfold Cong_3 in *; spliter; repeat split; Between; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch04_cong_bet