proposition: Lemma col_conga_col : forall A B C D E F, Col A B C -> CongA A B C D E F -> Col D E F.
proof: Proof. intros. induction H. assert (Bet D E F). eapply bet_conga__bet. apply H. assumption. unfold Col. left. assumption. induction H. assert (Out E D F). apply (l11_21_a A B C); [|apply H0]. apply bet_out in H. apply l6_6. assumption. unfold CongA in H0. spliter. assumption. unfold Out in H1. spliter. unfold Col. induction H3. right; right. apply between_symmetry. assumption. right; left. assumption. assert (Out E D F). apply (l11_21_a A B C); [|apply H0]. apply between_symmetry in H. apply bet_out. unfold CongA in H0. spliter. auto. assumption. unfold Out in H1. spliter. unfold Col. induction H3. right; right. apply between_symmetry. assumption. right; left. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2