proposition: Lemma sac_perm : forall A B C D, Saccheri A B C D -> Saccheri D C B A.
proof: Proof. intros. unfold Saccheri in *. spliter. repeat split; Perp; Cong; Side. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma