proposition: Lemma lam__pars1423 : forall A B C D, Lambert A B C D -> Par_strict A D B C.
proof: Proof. intros; apply par_strict_right_comm, lam__pars1234, lam_perm; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma