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