proposition: Lemma sac__par1423 : forall A B C D, Saccheri A B C D -> Par A D B C.
proof: Proof. intros A B C D HSac. apply par_strict_par, sac__pars1423, HSac. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma