proposition: Lemma per2_os__ncol234 : forall A B C D, Per B A D -> Per A D C -> OS A D B C -> ~ Col B C D.
proof: Proof. intros A B C D HPer1 HPer2 Hos. apply (par_strict_not_col_2 A), per2_os__pars; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma