proposition: Lemma sac__perp1214 : forall A B C D, Saccheri A B C D -> Perp A B A D.
proof: Proof. intros A B C D HSac. assert (Hdiff := sac_distincts A B C D HSac). unfold Saccheri in HSac; spliter. apply perp_left_comm, per_perp; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma