proposition: Lemma bet2_suma__suma : forall A B C D E F G H I A' D', A' <> B -> D' <> E -> Bet A B A' -> Bet D E D' -> SumA A B C D E F G H I -> SumA A' B C D' E F G H I.
proof: Proof. intros A B C D E F G H I A' D' HBA' HED' HBetA HBetD [J [HJ1 [HJ2 [HJ3 HJ4]]]]; spliter. destruct (segment_construction C B B C) as [C' []]. assert_diffs. apply (conga3_suma__suma A B C' D' E F G H I); [|apply l11_14; Between|CongA..]. exists J. split. apply l11_13 with C D; Between. repeat (split; trivial). intro; apply HJ2, col_one_side with C'; Col. apply coplanar_perm_3, col_cop__cop with C; Col; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles