proposition: Lemma sac_rectangle : forall A B C D, Saccheri A B C D -> Rectangle A B C D.
proof: Proof. intros A B C D H. assert (Parallelogram A B C D) by (apply sac_plg;auto). apply parallelogram_to_plg in H0. apply plg_per_rect1. assumption. unfold Saccheri in H. spliter; Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates