proposition: Lemma saccheri_s_three_hypotheses : hypothesis_of_acute_saccheri_quadrilaterals \/ hypothesis_of_right_saccheri_quadrilaterals \/ hypothesis_of_obtuse_saccheri_quadrilaterals.
proof: Proof. destruct ex_saccheri as [A [B [C [D HSac]]]]. assert(Hdiff := sac_distincts A B C D HSac). spliter. destruct (angle_partition A B C) as [|HUn]; [auto..| |right; destruct HUn]. left; apply (acute_sac__aah A B C D); trivial. left; apply (per_sac__rah A B C D); trivial. right; apply (obtuse_sac__oah A B C D); trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma