proposition: Lemma Cd_Col : forall O E S U1 U2 P X Y, Cd O E S U1 U2 P X Y -> Col O E X /\ Col O E Y.
proof: Proof. unfold Cd; unfold Projp; intros O E S U1 U2 P X Y HCd. destruct HCd as [HCs [HC [[PX HPX] [PY HPY]]]]; clear HC. destruct HPX as [[HDiff1 HElim1] HCong1]; destruct HPY as [[HDiff2 HElim2] HCong2]. split; [apply l4_13 with S U1 PX|apply l4_13 with S U2 PY]; Cong; [induction HElim1|induction HElim2]; spliter; treat_equalities; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths