proposition: Lemma sac__pars1234 : forall A B C D, Saccheri A B C D -> Par_strict A B C D.
proof: Proof. unfold Saccheri. intros A B C D HSac; spliter. apply per2_os__pars; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma