proposition: Lemma cong_3_3_cong_5: forall O E I J K S U X Y Z, O <> E -> Col O E I -> Col O E J -> Col O E K -> Cong_3 O E I S U X -> Cong_3 O E J S U Y -> Cong_3 O E K S U Z -> Cong_5 O E I J K S U X Y Z.
proof: Proof. intros O E I J K S U X Y Z HOE HCol1 HCol2 HCol3 HCong1 HCong4 HCong7. destruct HCong1 as [HCong1 [HCong2 HCong3]]. destruct HCong4 as [HCong4 [HCong5 HCong6]]. destruct HCong7 as [HCong7 [HCong8 HCong9]]. repeat (split; Cong); apply l4_16 with O E S U; Col; repeat (split; Cong). Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths