proposition: Lemma per_col : forall A B C D, B <> C -> Per A B C -> Col B C D -> Per A B D.
proof: Proof. unfold Per. intros. ex_and H0 C'. prolong D B D' D B. exists D'. assert (Midpoint B C C'). apply H0. induction H5. assert (Midpoint B D D') by (unfold Midpoint;split;Cong). assert (Midpoint B D D'). apply H7. induction H8. repeat split. assumption. Cong. unfold Col in H1. induction H1. assert (Bet B C' D'). eapply l7_15. eapply l7_3_2. apply H0. apply H7. assumption. assert (Cong C D C' D'). eapply l4_3_1. apply H1. apply H10. Cong. Cong. assert(OFSC B C D A B C' D' A) by (unfold OFSC;repeat split;Cong). apply cong_commutativity. eauto using five_segment_with_def. induction H1. assert (Bet C' D' B). eapply l7_15. apply H0. apply H7. apply l7_3_2. assumption. assert (Cong C D C' D') by (eapply l4_3 with B B;Between;Cong). assert(IFSC B D C A B D' C' A) by (unfold IFSC;repeat split;Between;Cong). apply cong_commutativity. eauto using l4_2. assert (Bet D' B C'). eapply l7_15. apply H7. eapply l7_3_2. apply H0. assumption. assert (Cong C D C' D') by (eapply l2_11 with B B;Between;Cong). assert(OFSC C B D A C' B D' A) by (unfold OFSC;repeat split;Between;Cong). apply cong_commutativity. eauto using five_segment_with_def. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR