proposition: Lemma l13_11 : forall A B C A' B' C' O, ~ Col O A A' -> B <> O -> C <> O -> Col O A B -> Col O B C -> B' <> O -> C' <> O -> Col O A' B' -> Col O B' C' -> Par B C' C B' -> Par C A' A C' -> Par A B' B A'.
proof: Proof. intros. assert (Coplanar B C' C O) by Cop. assert (Coplanar C A' A O) by (apply coplanar_perm_1, col_cop__cop with B; Col; Cop). assert(HH:=cop_par__perp2 B C' C B' O H10 H8). assert(HP:=cop_par__perp2 C A' A C' O H11 H9). assert(HQ : Perp2 A B' B A' O). apply(l13_10 A B C A' B' C' O); assumption. ex_and HQ X. ex_and H12 Y. assert_diffs. assert (Coplanar O A A' X). apply coplanar_perm_13, col_cop__cop with B'; Col. apply coplanar_perm_3, col_cop__cop with Y; Col; Cop. assert (Coplanar O A A' Y). apply coplanar_perm_13, col_cop__cop with B'; Col. apply coplanar_perm_3, col_cop__cop with X; Col; Cop. apply l12_9 with X Y; Perp; apply coplanar_pseudo_trans with O A A'; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch13_4_cos GeoCoq.Tarski_dev.Annexes.project