proposition: Lemma l11_57 : forall A B C A' B' C', OS A A' B B' -> Per B A A' -> Per B' A' A -> OS A A' C C' -> Per C A A' -> Per C' A' A -> CongA B A C B' A' C'.
proof: Proof. intros A B C A' B' C' HOSB HPer1 HPer2 HOSC HPer3 HPer4. destruct (midpoint_existence A A') as [M HM]. destruct (symmetric_point_construction B M) as [B'' HB'']. destruct (symmetric_point_construction C M) as [C'' HC'']. assert (HNColB := one_side_not_col123 A A' B B' HOSB). assert (HNColC := one_side_not_col123 A A' C C' HOSC). apply conga_trans with B'' A' C''. assert_diffs; apply symmetry_preserves_conga with M; auto. assert (~ Col B'' A A'). assert (B <> M) by (intro; subst; apply HNColB; Col); intro; apply HNColB; ColR. assert (Bet B'' A' B'). { assert (Col B' B'' A'). { assert_diffs; apply (cop_per2__col A); auto. apply coplanar_perm_3, coplanar_trans_1 with B; [Col|Cop|]. exists M; right; right; split; Col. apply midpoint_preserves_per with B A A' M; Midpoint. } apply col_two_sides_bet with A; Col. apply invert_two_sides, l9_2, l9_8_2 with B; trivial. repeat split; Col. exists M; split; [Col|Between]. } assert (~ Col C'' A A'). assert (C <> M) by (intro; subst; apply HNColC; Col); intro; apply HNColC; ColR. assert (Bet C'' A' C'). { assert (Col C' C'' A'). { assert_diffs; apply (cop_per2__col A); auto. apply coplanar_perm_3, coplanar_trans_1 with C; [Col|Cop|]. exists M; right; right; split; Col. apply midpoint_preserves_per with C A A' M; Midpoint. } apply col_two_sides_bet with A; Col. apply invert_two_sides, l9_2, l9_8_2 with C; trivial. repeat split; Col. exists M; split; [Col|Between]. } apply one_side_not_col124 in HOSB. apply one_side_not_col124 in HOSC. assert_diffs; apply l11_14; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2