proposition: Lemma lam__par1234 : forall A B C D, Lambert A B C D -> Par A B C D.
proof: Proof. intros A B C D HLam. apply par_strict_par, lam__pars1234, HLam. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma