proposition: Lemma ncol124_plg__pars1423 : forall A B C D, ~ Col A B D -> Parallelogram A B C D -> Par_strict A D B C.
proof: Proof. intros; apply plgs_pars_2; apply ncol124_plg__plgs; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates