proposition: Lemma per2_os__pars : forall A B C D, Per B A D -> Per A D C -> OS A D B C -> Par_strict A B C D.
proof: Proof. intros A B C D HPer1 HPer2 Hos. assert_diffs. assert(~ Col A D B) by (apply (one_side_not_col123 _ _ _ C), Hos). apply (col_cop_perp2__pars D A); Perp; Col; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma