proposition: Lemma lam_obtuse__oah : forall A B C D, Lambert A B C D -> (Obtuse B C D <-> hypothesis_of_obtuse_saccheri_quadrilaterals).
proof: Proof. intros A B C D HLam. assert(HC' := symmetric_point_construction C B). destruct HC' as [C']. assert(HD' := symmetric_point_construction D A). destruct HD' as [D']. split. - intro. apply (obtuse_sac__oah D C C' D'). apply (lam6521_mid2__sac _ _ _ _ B A); auto. unfold Lambert in HLam. spliter. assert_diffs. apply (conga_obtuse__obtuse B C D); auto. apply conga_left_comm, out2__conga; [apply out_trivial|apply l6_6, bet_out]; Between. - intro oah. apply (conga_obtuse__obtuse D C C'); auto. apply (oah _ _ _ D'); apply (lam6521_mid2__sac _ _ _ _ B A); auto. unfold Lambert in HLam. spliter. assert_diffs. apply conga_left_comm, out2__conga; [apply bet_out|apply out_trivial]; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma