proposition: Lemma lam_per__rah : forall A B C D, Lambert A B C D -> (Per B C D <-> hypothesis_of_right_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 (per_sac__rah D C C' D'). apply (lam6521_mid2__sac _ _ _ _ B A); auto. unfold Lambert in HLam. spliter. apply l8_2. apply (l8_3 B); Col. - intro rah. apply (l8_3 C'); Col ;[|unfold Lambert in HLam; spliter; assert_diffs; auto]. apply l8_2. apply (rah _ _ _ D'). apply (lam6521_mid2__sac _ _ _ _ B A); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma