proposition: Lemma l11_61 : forall A B C A' B' C', A <> A' -> A <> B -> A <> C -> Coplanar A A' B B' -> Per B A A' -> Per B' A' A -> Coplanar A A' C C' -> Per C A A' -> Per B A C -> Per B' A' C'.
proof: Proof. intros A B C A' B' C'; intros. assert (~ Col C A A') by (assert_diffs; apply per_not_col; auto). destruct (l10_15 A A' A' C) as [C'' []]; Col. assert_diffs. apply l8_2, (l11_60 A' A C''); [apply one_side_not_col124 with C; Side|Perp..| |apply coplanar_trans_1 with C; Col; Cop]. apply l8_2. revert dependent B'. assert (Haux : forall B', OS A A' B B' -> Per B' A' A -> Per B' A' C''). { intros B' HOS HPer. apply (l11_17 B A C); trivial. apply l11_57; Perp. } intro B'; intros. destruct (eq_dec_points B' A'); [subst; Perp|]. assert (HNCol : ~ Col B' A' A) by (apply per_not_col; auto). destruct (cop__one_or_two_sides A A' B B'); Col. apply per_not_col; auto. destruct (segment_construction B' A' A' B') as [B'' []]. assert_diffs. apply l8_2, per_col with B''; Col. apply l8_2, Haux; [|apply l8_2, per_col with B'; Perp; Col]. exists B'; split; trivial. repeat split; Col. intro; apply HNCol; ColR. exists A'; split; Col; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2