proposition: Lemma lam__pars1234 : forall A B C D, Lambert A B C D -> Par_strict A B C D.
proof: Proof. unfold Lambert. intros A B C D HLam. spliter. assert (~ Col B A D) by (apply per_not_col; auto). apply (col_cop_perp2__pars D A); Perp; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma