proposition: Lemma sac__perp3414 : forall A B C D, Saccheri A B C D -> Perp C D A D.
proof: Proof. intros A B C D HSac. apply perp_comm, (sac__perp1214 _ _ B), sac_perm; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma