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