proposition: Lemma per_sac__rah : forall A B C D, Saccheri A B C D -> Per A B C -> hypothesis_of_right_saccheri_quadrilaterals.
proof: Proof. intros A B C D HSac HPer A' B' C' D' HSac'. assert(HM := midpoint_existence B C). assert(HM' := midpoint_existence B' C'). assert(HN := midpoint_existence A D). assert(HN' := midpoint_existence A' D'). destruct HM as [M]. destruct HM' as [M']. destruct HN as [N]. destruct HN' as [N']. elim(le_cases M N M' N'); intro Hle; [assert(Haux := three_hypotheses_aux A B C D M N A' B' C' D' M' N') |assert(Haux := three_hypotheses_aux A' B' C' D' M' N' A B C D M N)]; destruct Haux as [[] _]; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma